# Kerodon

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

Remark 7.4.1.2. In the situation of Theorem 7.4.1.1, the restriction map $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}^{\triangleleft } }^{\operatorname{CCart}}( \operatorname{\mathcal{C}}^{\triangleleft }, \overline{\operatorname{\mathcal{E}}} ) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is automatically an isofibration of $\infty$-categories (Remark 5.3.1.18). Using Proposition 4.5.5.20, we see that condition $(1)$ of Theorem 7.4.1.1 is equivalent to the following a priori stronger condition:

$(1')$

The restriction map

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

is a trivial Kan fibration of simplicial sets.