Remark 5.3.1.18 (02T5)

Remark 5.3.1.18. In the situation of Remark 5.3.1.17, suppose that $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ is a monomorphism of simplicial sets. Then the restriction map $F^{\ast }: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 )$ is an isofibration. To see this, we first observe that $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}})$ can be regarded as a replete subcategory of the fiber product

\[ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }^{\operatorname{CCart}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ) \times _{ \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ) } \operatorname{Fun}_{ /\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \]

(Remark 5.3.1.15). It will therefore suffice to show that the restriction map

\[ \operatorname{Fun}_{ /\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}', \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_0 }( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}_0 ) \simeq \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( \operatorname{\mathcal{E}}'_0, \operatorname{\mathcal{E}}) \]

is an isofibration, which follows from Proposition 4.5.5.14.