Kerodon

Remark 8.5.1.16. In the situation of Proposition 8.5.1.15, suppose that the $\infty $-category $\operatorname{\mathcal{X}}$ is a Kan complex. Then $\operatorname{\mathcal{Y}}$ is also a Kan complex, and is therefore a retract of $X$ in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. To prove this, it will suffice to show that every morphism $f: Y \rightarrow Y'$ in the $\infty $-category $\operatorname{\mathcal{Y}}$ is an isomorphism (Proposition 4.4.2.1). Since $\operatorname{\mathcal{X}}$ is a Kan complex, the morphism $i(f): i(Y) \rightarrow i(Y')$ is an isomorphism in $\operatorname{\mathcal{X}}$ (Proposition 1.4.6.10). It follows that $(r \circ i)(f)$ is an isomorphism in $\operatorname{\mathcal{Y}}$ (Remark 1.5.1.6). Since $f$ is isomorphic to $(r \circ i)(f)$ (as an object of the $\infty $-category $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{Y}})$), it is also an isomorphism (Example 4.4.1.14).