# Kerodon

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

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$