Kerodon

Proof of Theorem 8.1.3.14. Let $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ be categories, where $\operatorname{\mathcal{C}}$ admits pushouts, and let $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{Cospan}(\operatorname{\mathcal{C}})$ be a strictly unitary lax functor of $2$-categories. For every morphism $f: X \rightarrow Y$ in the category $\operatorname{\mathcal{D}}$, we can identify $G(f)$ with a cospan from $G(X)$ to $G(Y)$ in the category $\operatorname{\mathcal{C}}$, given by a diagram we will denote by $G(X) \xrightarrow { b_{-}(f) } B(f) \leftarrow { b_{+}(f) } G(Y)$. Our assumption that $G$ is strictly unitary guarantees the following:

$(\ast )$

For each object $X \in \operatorname{\mathcal{D}}$, the object $B( \operatorname{id}_ X )$ is equal to $G(X)$, and the maps $b_{-}(\operatorname{id}_ X): G(X) \rightarrow B( \operatorname{id}_ X )$ and $b_{+}( \operatorname{id}_ X): G( X) \rightarrow B( \operatorname{id}_ X )$ are the identity morphisms from $G(X)$ to itself in the category $\operatorname{\mathcal{C}}$.

For every pair of composable $1$-morphisms $X \xrightarrow {f} Y \xrightarrow {g} Z$, the composition constraint $\mu _{g,f}$ for the lax functor $G$ can be identified with a morphism from the pushout $B(f) \amalg _{ G(Y) } B(g)$ to $B( g \circ f)$, or equivalently with a pair of morphisms

satisfying $p(g,f) \circ b_{+}(f) = q(g,f) \circ b_{-}(g)$. The axioms for a lax functor (Definition 2.2.4.5) then translate to the following additional conditions:

$(a)$

For every morphism $f: X \rightarrow Y$ in the category $\operatorname{\mathcal{D}}$, $p( \operatorname{id}_ Y, f)$ is the identity morphism from $B(f)$ to itself.

$(b)$

For every morphism $f: X \rightarrow Y$ in the category $\operatorname{\mathcal{D}}$, $q( f, \operatorname{id}_ X )$ is the identity morphism from $B(f)$ to itself.

$(c)$

For every composable triple of $1$-morphisms $W \xrightarrow {f} X \xrightarrow {g} Y \xrightarrow {h} Z$ in the category $\operatorname{\mathcal{D}}$, we have

\[ p(h \circ g, f) = p( h, g \circ f) \circ p(g,f) \quad \quad q(h, g \circ f ) = q(h \circ g, f) \circ q(h,g) \]

\[ p( h, g \circ f) \circ q(g,f) = q(h \circ g, f) \circ p( h, g). \]

We wish to show that there exists a unique functor of ordinary categories $F: \operatorname{Tw}(\operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{C}}$ such that $G = F^{+}$, where $F^{+}$ is the lax functor associated to $F$ by Construction 8.1.3.12. For this condition to be satisfied, the functor $F$ must satisfy the following conditions:

$(0)$

For each object $X \in \operatorname{\mathcal{D}}$, we have $F( \operatorname{id}_ X ) = G(X)$ (this guarantees that $G$ and $F^{+}$ coincide on objects).

$(1)$

For each morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{D}}$ (regarded as an object of $\operatorname{Tw}(\operatorname{\mathcal{D}})$), we have $F(f) = B(f)$, and the morphisms $b_{-}(f)$ and $b_{+}(f)$ are given by $F( \operatorname{id}_ X, f)$ and $F(f, \operatorname{id}_ Y)$, respectively (this guarantees that $G$ and $F^{+}$ coincide on $1$-morphisms, and therefore also on $2$-morphisms).

$(2)$

For every pair of composable $1$-morphisms $X \xrightarrow {f} Y \xrightarrow {g} Z$, the morphisms $p(g,f): B(f) \rightarrow B(g \circ f)$ and $q(g,f): B(g) \rightarrow B(g \circ f)$ are given by $F(\operatorname{id}_ X,g): F(f) \rightarrow F(g \circ f)$ and $F(f, \operatorname{id}_ Z): F(g) \rightarrow F(g \circ f)$, respectively (this guarantees that the composition constraints on $G$ and $F^{+}$ coincide).

Note that the value of $F$ on each object of $\operatorname{Tw}(\operatorname{\mathcal{D}})$ is determined by condition $(1)$. Moreover, if $(u,v)$ is a morphism from $f: X \rightarrow Y$ to $f': X' \rightarrow Y'$ in the category $\operatorname{Tw}(\operatorname{\mathcal{D}})$, then condition $(2)$ guarantees that $F(u,v)$ must be equal to the composition

This proves the uniqueness of the functor $F$.

To prove existence, we define $F$ on objects $f$ of $\operatorname{Tw}(\operatorname{\mathcal{D}})^{\operatorname{op}}$ by the formula $F(f) = B(f)$, and on morphisms $(u,v): f \rightarrow f'$ by the formula $F(u,v) = p(v, f \circ u) \circ q(f,u)$. For any morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$, we can use $(a)$ and $(b)$ to compute

so that $F$ carries identity morphisms in $\operatorname{Tw}(\operatorname{\mathcal{D}})$ to identity morphisms in $\operatorname{\mathcal{C}}$. To complete the proof that $F$ is a functor, we note that for every pair of composable morphisms

in the twisted arrow category $\operatorname{Tw}(\operatorname{\mathcal{D}})$, the identities given in $(c)$ allow us to compute

We now complete the proof by showing that the functor $F$ satisfies conditions $(0)$, $(1)$, and $(2)$. Condition $(0)$ is an immediate consequence of $(\ast )$. To prove $(2)$, we note that for any pair of composable morphisms $X \xrightarrow {f} Y \xrightarrow {g} Z$ in $\operatorname{\mathcal{D}}$, identities $(a)$ and $(b)$ yield equalities

To prove $(1)$, we note that if $f: X \rightarrow Y$ is a morphism in $\operatorname{\mathcal{D}}$, then we have

and a similar calculation yields $F(f, \operatorname{id}_ Y) = b_{+}(f)$. $\square$