Proposition 5.1.7.11. 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.7.1).
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof of Proposition 5.1.7.11. Since $F$ and $G$ are isomorphic 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.7.9); in this case, we wish to show that both inclusion maps are equivalences of $\infty $-categories (Corollary 5.1.7.8). This follows by applying Corollary 4.5.2.29 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$