$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 7.4.5.12. Suppose we are given a pullback diagram of small simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d]^{U} & \overline{\operatorname{\mathcal{E}}} \ar [d]^{ \overline{U} } \ar [d] \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{C}}^{\triangleright }, } \]
where $U$ and $\overline{U}$ are left fibrations. The following conditions are equivalent:
- $(1)$
The inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is a weak homotopy equivalence of simplicial sets.
- $(2)$
The covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{S}}$ is a colimit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$.
Proof.
Let ${\bf 1}$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright }$, and let $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } = \{ {\bf 1} \} \times _{\operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ denote the corresponding fiber of $\overline{\operatorname{\mathcal{E}}}$. Since the inclusion map $\{ {\bf 1} \} \hookrightarrow \operatorname{\mathcal{C}}^{\triangleright }$ is right anodyne (Example 4.3.7.11), the inclusion $\iota : \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} } \hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is also right anodyne (Corollary 7.2.3.14). In particular, $\iota $ is a weak homotopy equivalence of simplicial sets. Let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ be a covariant refraction diagram (Proposition 7.4.3.3), so that the inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is homotopic to the composition $\iota \circ \mathrm{Rf}$. It follows that condition $(1)$ can be reformulated as follows:
- $(1')$
The covariant refraction diagram $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ is a weak homotopy equivalence.
The equivalence $(1') \Leftrightarrow (2)$ follows by combining Proposition 7.4.5.1, Theorem 7.4.3.6, and Proposition 6.3.1.20.
$\square$