Kerodon

Corollary 3.2.6.5. Let $f: X \rightarrow S$ be a Kan fibration between Kan complexes, let $s$ be a vertex of $S$, and set $X_{s} = \{ s\} \times _{S} X$. Then two elements of $\pi _0( X_ s )$ have the same image in $\pi _0( X )$ if and only if they belong to the same orbit of the action of the fundamental group $\pi _{1}(S,s)$ (see Variant 3.2.5.5). In other words, the inclusion of Kan complexes $X_{s} \hookrightarrow X$ induces a monomorphism of sets $(\pi _{1}(S,s) \backslash \pi _{0}(X_ s)) \hookrightarrow \pi _0(X)$.