# Kerodon

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

Corollary 5.7.2.21. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ be a morphism of simplicial sets, let $U: \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}$ be the cocartesian fibration of Proposition 5.7.2.2, and let

$f_{!}: \{ C\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \{ D\} \times _{\operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F}$

be a functor which is given by covariant transport along an edge $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$ (Definition 5.2.2.4). Then the diagram

$\xymatrix@R =50pt@C=50pt{ \mathscr {F}(C) \ar [d]^{ [\mathscr {F}(f)]} \ar [r]^-{\sim } & \{ C\} \times _{ \operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F} \ar [d]^{ [ f_{!} ] } \\ \mathscr {F}(D) \ar [r]^-{\sim } & \{ D\} \times _{ \operatorname{\mathcal{C}}} \int _{\operatorname{\mathcal{C}}} \mathscr {F} }$

commutes in the homotopy category $\mathrm{h} \mathit{\operatorname{QCat}}$ (where the horizontal maps are the equivalences described in Example 5.7.2.18).

Proof. Without loss of generality, we may assume that $\operatorname{\mathcal{C}}= \Delta ^1$, in which case the desired result reduces to Proposition 5.7.2.20. $\square$