Kerodon

“... so that $h_0$ can be identified with [a] morphism ...”

There is something wrong with the last sentence of the proof. Probably one should delete “the edge of $X$”.

Yep. Thanks!

I am wondering whether the following extension of the proposition holds true:

Let $q\colon X\to S$ be a cartesian fibration (for simplicity) and $n\ge 2$. Denote $\operatorname{Fun}'(\Delta^n, X) \subseteq \operatorname{Fun}(\Delta^n,X)$ the full simplicial subset spanned by those $n$-simplices $\sigma\colon \Delta^n \to X$ for which the composition $\Delta^1 \simeq \\{n-1\to n\\} \subseteq \Delta^n \xrightarrow{\sigma} X$ classifies a $q$-cartesian edge. Define $\operatorname{Fun}'(\Lambda^n_n, X) \subseteq \operatorname{Fun}(\Lambda^n_n,X)$ similarly. Is the natural map $$\operatorname{Fun}'(\Delta^n, X) \to \operatorname{Fun}'(\Lambda^n_n, X) \times_{\operatorname{Fun}(\Lambda^n_n,S)} \operatorname{Fun}(\Delta^n, S)$$ a trivial Kan fibration?

Yes, this is also true.