Is the overcategory $C_{/p}$ a subcategory of the $\infty$-category $\operatorname{Fun}(K^{\vartriangleleft}, C)$? Let $p: K \to C$ be a simplicial morphism from a simplicial set $K$ to an $\infty$-category $C$.
$\newcommand{\catSSet}{\mathtt{SSet}}\DeclareMathOperator{\Fun}{Fun}$
The over $\infty$-category $C_{/p}$ is defined as the simplicial set
$$ (C_{/p})_n = \catSSet_p( \Delta^n \star K, C) $$
where the RHS is the set of simplicial maps that restrict to $p$ via the natural map $K \to \Delta^n \star K$.
My question is that, can this category be characterized as a simplicial subset of
$$ \Fun( K^{\vartriangleleft}, C) : [n] \mapsto \catSSet(K^{\vartriangleleft} \times \Delta^n, C) $$
where $K^{\vartriangleleft}:= \Delta^0 \star K$ is the left cone over $K$.
If yes, how to define it componentwise directly (without  involving the general join construction)? 
(The origin of my question is that, the over category should be "the category of cones that restrict to the given diagram", but I am not sure how to rigorously phrase the condition "restrict to the given diagram" for $n$-simplices with $n\geq 1$ -- though I know the above definition involving join construction should be the correct way, but I am just curious about if there is any other description.)
 A: There is an epimorphism $q : \Delta^n \times K^{\triangleleft} \to \Delta^n \star K$ that projects $\Delta^n \times \{v\}$ onto its first component $\Delta^n$ ( - $v$ shall denote the cone point of $K^{\triangleleft}$ - ) and $\Delta^n \times K$ onto its second component $K$. So I would say: yes, the $\infty$-category $\mathcal{C}_{/p}$ is a simplicial subset of the $\infty$-category $\mathcal{C}^{K^{\triangleleft}}$. It is precisely the inverse image of $p \in \mathcal{C}^K$ with respect to the canonical map $\mathcal{C}^{K^{\triangleleft}} \to \mathcal{C}^K$, i.e. $\mathcal{C}_{/p} = \mathcal{C}^{K^{\triangleleft}} \times_{\mathcal{C}^K} \{p\}$.
To prove that the inverse image is contained in $\mathcal{C}_{/p}$, you have to show that every map $f : \Delta^n \times K^{\triangleleft} \to \mathcal{C}$ that has the property that $f_{|\Delta^n \times K} = p \circ pr_2$ ( - where $pr_2 : \Delta^n \times K \to K$ is the projection onto the second component - ) lifts (uniquely) along $q$ to a map $f' : \Delta^n \star K \to \mathcal{C}$ such that $f'_{|K} = p$. The other direction ( - that $\mathcal{C}_{/p}$ is contained in the inverse image - ) is easier.
