# Kerodon

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

Corollary 5.6.7.7. Suppose we are given a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}\ar [rr]^-{F} \ar [dr]_{U} & & \operatorname{\mathcal{E}}\ar [dl]^{V} \\ & \operatorname{\mathcal{C}}, & }$

where $U$ and $V$ are cocartesian fibrations. Then $F$ is an equivalence of cocartesian fibrations over $\operatorname{\mathcal{C}}$ (Definition 5.1.6.1) if and only if it is a categorical equivalence of simplicial sets.

Proof. Combine Proposition 5.1.6.5 with Corollary 5.6.7.5. $\square$