Kerodon

Proof. We will prove the first assertion; the proof of the second is similar. Let $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ be a unitary lax functor of $2$-categories. Suppose we are given an object $(D,Y)$ of the Grothendieck construction $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$, so that $D$ is an object of the category $\operatorname{\mathcal{C}}$ and $Y$ is an object of the category $\mathscr {F}(D)$. For every morphism $f: C \rightarrow D$ in the category $\operatorname{\mathcal{C}}$, we can choose an isomorphism $u: X \rightarrow \mathscr {F}(f)(Y)$ in the category $\mathscr {F}(C)$ (for example, we can take $X = \mathscr {F}(f)(Y)$ and $u$ to be the identity morphism). Then $(f,u)$ is a morphism from $(C,X)$ to $(D,Y)$ in the category $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$, and our assumption that $\mathscr {F}$ is unitary guarantees that $(f,u)$ is locally $U$-cartesian (Example 11.10.3.7). This proves that $U$ is a locally cartesian fibration of categories. Suppose that we are given another locally $U$-cartesian morphism $(g, v): (D,Y) \rightarrow (E,Z)$ in $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$, so that $g: D \rightarrow E$ is a morphism in $\operatorname{\mathcal{C}}$ and $v: Y \simeq \mathscr {F}(g)(Z)$ is an isomorphism in the category $\mathscr {F}(D)$ (Example 11.10.3.7). The composition $(g,v) \circ (f,u)$ can then be identified with $(g \circ f, w)$, where $w$ is given by the composition

here $\mu _{f,g}$ denotes the composition constraint for the lax functor $\mathscr {F}$. Invoking Example 11.10.3.7 again, we conclude that $(g,v) \circ (f,u)$ is locally $U$-cartesian if and only if $\mu _{f,g}(Z)$ is an isomorphism. Allowing $f$, $g$, and $Z$ to vary (and invoking the criterion of Proposition 11.10.3.13), we conclude that $U$ is a cartesian fibration if and only if each of the composition constraints $\mu _{f,g}$ is an isomorphism: that is, if and only if the lax functor $\mathscr {F}$ is a functor. $\square$

Proof. The implication $(2) \Rightarrow (1)$ is immediate from the definition. We now show that $(1) \Rightarrow (2)$. Assume that $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ is a cartesian fibration of categories. Then $U$ is also a locally cartesian fibration (Example 11.10.3.11). Let $f: X \rightarrow Y$ be a locally $U$-cartesian morphism in $\operatorname{\mathcal{D}}$. Since $U$ is a cartesian fibration, we can choose a $U$-cartesian morphism $f': X' \rightarrow Y$ satisfying $U(X') = U(X)$ and $U(f') = U(f)$. Using our assumption that $f$ is locally $U$-cartesian, we deduce that $f'$ factors uniquely as a composition $f \circ e$, where $e: X' \rightarrow X$ has the property that $U(e) = \operatorname{id}_{ U(X)}$. Since $f'$ is locally $U$-cartesian, the morphism $e$ is an isomorphism (Remark 11.10.3.6). Applying Remark ***, we deduce that $f = f' \circ e^{-1}$ is also $U$-cartesian.

The implication $(2) \Rightarrow (3)$ follows from Remark ***. We will complete the proof by showing that $(3) \Rightarrow (2)$. Assume that $U$ is a locally cartesian fibration of categories and that the collection of locally $U$-cartesian morphisms of $\operatorname{\mathcal{D}}$ is closed under composition. Let $g: X \rightarrow Y$ be a locally $U$-cartesian morphism in $\operatorname{\mathcal{D}}$; we wish to show that $g$ is $U$-cartesian. Fix an object $W \in \operatorname{\mathcal{D}}$ and a morphism $\overline{f}: U(W) \rightarrow U(X)$, so that postcomposition with $g$ induces a function

We wish to show that $\theta $ is a bijection. To prove this, we invoke our assumption that $U$ is a locally cartesian fibration to choose a locally $U$-cartesian morphism $f': W' \rightarrow X$ in $\operatorname{\mathcal{D}}$ satisfying $U(W') = U(W)$ and $U(f') = \overline{f}$. We then have a commutative diagram

Since $f'$ and $g \circ f'$ are locally $U$-cartesian, the vertical maps in this diagram are bijections. It follows that $\theta $ is also a bijection, as desired. $\square$