# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Proposition 5.1.6.10. Let $V: \widetilde{\operatorname{\mathcal{D}}} \rightarrow \operatorname{\mathcal{D}}$ be an isofibration of $\infty$-categories, let $\operatorname{\mathcal{C}}$ be a simplicial set, and let $F,G: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be morphisms of simplicial sets which are isomorphic when viewed as objects of the $\infty$-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$. Then the isofibrations $F^{\ast }( \widetilde{\operatorname{\mathcal{D}}} ) \rightarrow \operatorname{\mathcal{C}}$ and $G^{\ast }( \widetilde{\operatorname{\mathcal{D}}} ) \rightarrow \operatorname{\mathcal{C}}$ are equivalent (in the sense of Definition 5.1.6.1).

Proof of Proposition 5.1.6.10. Since $F$ and $G$ are isomorphism as objects of $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$, there exists a contractible Kan complex $X$ containing vertices $f$ and $g$ and a functor $H: X \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ satisfying $H(f) = F$ and $H(g) = G$. Let us identify $H$ with a morphism of simplicial sets $X \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$, and let $\widetilde{\operatorname{\mathcal{C}}}$ denote the fiber product $(X \times \operatorname{\mathcal{C}}) \times _{\operatorname{\mathcal{D}}} \widetilde{\operatorname{\mathcal{D}}}$. We will show that the inclusion maps

$F^{\ast }( \widetilde{\operatorname{\mathcal{D}}} ) = \{ f\} \times _{X} \widetilde{\operatorname{\mathcal{C}}} \hookrightarrow \widetilde{\operatorname{\mathcal{C}}} \hookleftarrow \{ g\} \times _{X} \widetilde{\operatorname{\mathcal{C}}} = G^{\ast }( \widetilde{\operatorname{\mathcal{D}}})$

are equivalences of inner fibrations over $\operatorname{\mathcal{C}}$. To prove this, we may assume without loss of generality that $\operatorname{\mathcal{C}}= \Delta ^ n$ is a standard simplex (Proposition 5.1.6.9); in this case, we wish to show that both inclusion maps are equivalences of $\infty$-categories (Corollary 5.1.6.8). This follows by applying Corollary 4.5.2.23 to the diagram of pullback squares

$\xymatrix@R =50pt@C=50pt{ F^{\ast }(\widetilde{\operatorname{\mathcal{D}}}) \ar [r] \ar [d] & \widetilde{\operatorname{\mathcal{C}}} \ar [d] & G^{\ast }(\widetilde{\operatorname{\mathcal{D}}}) \ar [l] \ar [d] \\ \{ f\} \times \operatorname{\mathcal{C}}\ar [r] & X \times \operatorname{\mathcal{C}}& \{ g\} \times \operatorname{\mathcal{C}}; \ar [l] }$

here the vertical maps are isofibrations (since they are pullbacks of $V$) and the lower horizontal maps are equivalences of $\infty$-categories (since $X$ is a contractible Kan complex). $\square$