Kerodon

Proof. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. We wish to show that precomposition with $f$ induces a bijection

Let $s: Y \rightarrow X$ be a section of $f$ (so that $f \circ s = \operatorname{id}_{Y}$). Then precomposition with $s$ induces a function $s^{\ast }: \pi _0(\operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq }) \rightarrow \pi _0( \operatorname{Fun}(Y, \operatorname{\mathcal{C}})^{\simeq } )$ for which the composition $s^{\ast } \circ f^{\ast }$ is equal to the identity on the set $\pi _0( \operatorname{Fun}(Y, \operatorname{\mathcal{C}})^{\simeq } )$. We will complete the proof by showing that the composition $f^{\ast } \circ s^{\ast }$ is isomorphic to the identity on $\pi _0( \operatorname{Fun}(X, \operatorname{\mathcal{C}})^{\simeq } )$. Fix a map of simplicial sets $g: X \rightarrow \operatorname{\mathcal{C}}$; we wish to show that $g$ is isomorphic to the composite map

as an object of the $\infty $-category $\operatorname{Fun}(X, \operatorname{\mathcal{C}})$.

Since $f$ is a trivial Kan fibration, the composition $s \circ f$ is fiberwise homotopic to the identity map $\operatorname{id}_{X}$: that is, we can choose a morphism of simplicial sets $h: \Delta ^1 \times X \rightarrow X$ which is compatible with the projection to $Y$ and which satisfies $h|_{ \{ 0\} \times X } = s \circ f$ and $h|_{\{ 1\} \times X} = \operatorname{id}_{X}$. The composition $g \circ h$ can then be regarded as a natural transformation $u: (g \circ s \circ f) \rightarrow g$. We will complete the proof by showing that $u$ is an isomorphism in the $\infty $-category $\operatorname{Fun}(X, \operatorname{\mathcal{C}})$. By virtue of Theorem 4.4.4.4, it will suffice to prove that for each vertex $x \in X$, the composite map

describes an invertible morphism in $\operatorname{\mathcal{C}}$. Setting $y = f(x)$, we note that this composite map factors through the (contractible) Kan complex $X_{y}$, so the desired result follows from Proposition 1.4.6.10. $\square$