# Kerodon

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

Corollary 7.4.5.10. 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}}^{\triangleleft }, }$

where $U$ and $\overline{U}$ are left fibrations. The following conditions are equivalent:

$(1)$

The restriction map

$\operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$

is a homotopy equivalence of Kan complexes.

$(2)$

The covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleleft } }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{\mathcal{S}}$ is a limit diagram in the $\infty$-category $\operatorname{\mathcal{S}}$.

Proof. Since $\overline{U}$ is a left fibration, every edge of $\overline{\operatorname{\mathcal{E}}}$ is $\overline{U}$-cocartesian (Example 5.1.1.3). We can therefore identify $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} )$ and $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ with the $\infty$-categories $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} )$ and $\operatorname{Fun}^{\operatorname{CCart}}_{ / \operatorname{\mathcal{C}}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$, respectively. The desired result now follows by combining Theorem 7.4.1.1 with Proposition 7.4.5.1. $\square$