Kerodon

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

Remark 11.10.2.8. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a locally cartesian fibration of categories which is equipped with a cleavage $(f,Y) \mapsto \widetilde{f}_{Y}$. The following conditions are equivalent:

  • Whenever $f = \operatorname{id}_{C}$ is an identity morphism in the category $\operatorname{\mathcal{C}}$, the morphism $\widetilde{f}_{Y}$ is equal to $\operatorname{id}_{Y}$ for each $Y \in \operatorname{\mathcal{E}}_{C}$.

  • The transport representation $\chi _{U}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ of Construction 11.10.2.4 is strictly unitary (Definition 2.2.4.17).

Note that it is always possible to choose a cleavage $(f,Y) \mapsto \widetilde{f}_{Y}$ which satisfies these conditions.