Kerodon

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

Remark 11.10.2.7. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a locally cartesian fibration of categories. For every cleavage $(f,Y) \mapsto \widetilde{f}_{Y}$ of $U$, the transport representation $\chi _{U}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ is a unitary lax functor: that is, each of the identity constraints $\epsilon _{C}: \operatorname{id}_{\chi _{U}(C)} \rightarrow \chi _{U}( \operatorname{id}_{C} )$ is an isomorphism.