Proof of Theorem 8.1.8.4.
Let $\operatorname{\mathcal{A}}$ be an ordinary category, let $\operatorname{\mathcal{C}}$ be a $2$-category containing objects $X$ and $Y$, and let $U: [1] \times \operatorname{\mathcal{A}}\rightarrow \operatorname{\mathcal{C}}$ be a strictly unitary lax functor having the property that $U|_{ \{ 0\} \times \operatorname{\mathcal{A}}}$ and $U|_{ \{ 1\} \times \operatorname{\mathcal{A}}}$ are the constant functors taking the values $X$ and $Y$, respectively. We wish to show that there exists a unique functor of ordinary categories $F: \operatorname{Tw}(\operatorname{\mathcal{A}}) \rightarrow \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Y)$ such that $U$ is equal to the strictly unitary lax functor $U_{F}$ given by Construction 8.1.8.2. To prove this, we may assume without loss of generality that the $2$-category $\operatorname{\mathcal{C}}$ is strictly unitary (Proposition 2.2.7.7). Given a morphism $f: A \rightarrow B$ in the category $\operatorname{\mathcal{A}}$ and a pair of integers $0 \leq i \leq j \leq 1$, we write $f_{ji}: (i,A) \rightarrow (j,B)$ for the corresponding morphism in the product category $[1] \times \operatorname{\mathcal{A}}$. Unwinding the definitions, we see that the identity $U = U_{F}$ imposes the following requirements on the functor $F$:
- $(1)$
Let $f: A \rightarrow B$ be a morphism in the category $\operatorname{\mathcal{C}}$, which we identify with an object of the twisted arrow category $\operatorname{Tw}(\operatorname{\mathcal{A}})$. Then $F(f)$ is equal to $U( f_{10} ) \in \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Y)$.
- $(2)$
Let $f: A \rightarrow B$ and $g: B \rightarrow C$ be composable morphisms in the category $\operatorname{\mathcal{A}}$, and regard the pairs $(\operatorname{id}_ A, g)$ and $(f, \operatorname{id}_ C)$ as elements of $\operatorname{Hom}_{\operatorname{Tw}(\operatorname{\mathcal{A}})}(f, g \circ f)$ and $\operatorname{Hom}_{\operatorname{Tw}(\operatorname{\mathcal{A}})}( g, g \circ f)$, respectively. Then $F( \operatorname{id}_ A, g)$ and $F(f, \operatorname{id}_ C)$ are equal to the composition constraints $\mu _{ g_{11}, f_{10} }$ and $\mu _{ g_{10}, f_{00} }$ for the lax functor $U$, respectively.
We now establish the uniqueness of the functor $F$. The value of $F$ on objects is determined by condition $(1)$. If $f: A \rightarrow B$ and $f': A' \rightarrow B'$ are objects of the twisted arrow category $\operatorname{Tw}(\operatorname{\mathcal{A}})$, then an element of $\operatorname{Hom}_{\operatorname{Tw}(\operatorname{\mathcal{A}})}(f, f')$ can be identified with a pair $(u,v)$ where $u \in \operatorname{Hom}_{\operatorname{\mathcal{A}}}(A',A)$ and $v \in \operatorname{Hom}_{\operatorname{\mathcal{A}}}(B,B')$ satisfy $f' = v \circ f \circ u$. In this case, the morphism $(u,v)$ factors as a composition $(u, \operatorname{id}_{B'} ) \circ (\operatorname{id}_{A}, v)$, so condition $(2)$ guarantees the identity
\[ F(u,v) = F(u, \operatorname{id}_{B'} ) \circ F( \operatorname{id}_{A}, v) = \mu _{ (vf)_{10}, u_{00} } \circ \mu _{ v_{11}, f_{10} }. \]
This proves the uniqueness of $F$ on morphisms.
To prove existence, we define the functor $F$ on objects $f \in \operatorname{Tw}(\operatorname{\mathcal{A}})$ by setting $F(f) = U( f_{10} )$, and on morphisms $(u,v) \in \operatorname{Hom}_{\operatorname{Tw}(\operatorname{\mathcal{A}})}(f,f')$ by the formula
\[ F(u,v) = \mu _{ (vf)_{10}, u_{00} } \circ \mu _{ v_{11}, f_{10} }. \]
Note that this prescription automatically satisfies condition $(1)$. Since $U$ is a strictly unitary functor between strictly unitary $2$-categories, its composition constraints $\mu _{g,h}$ are the identity whenever either $g$ or $h$ is an identity morphism (Remark 2.2.7.5), which shows that $F$ satisfies condition $(2)$ and that it carries identity morphisms to identity morphisms. We will complete the proof by showing that $F$ is compatible with composition. Let $f: A \rightarrow B$, $f': A' \rightarrow B'$, and $f'': A'' \rightarrow B''$ be objects of the twisted arrow category $\operatorname{Tw}(\operatorname{\mathcal{A}})$, and suppose we are given morphisms $(u,v) \in \operatorname{Hom}_{\operatorname{Tw}(\operatorname{\mathcal{A}})}( f, f')$ and $(u',v') \in \operatorname{Hom}_{\operatorname{Tw}(\operatorname{\mathcal{A}})}( f',f'')$. We wish to prove an equality $F( u \circ u', v' \circ v) = F(u',v') \circ F(u,v)$ of morphisms from $F(f)$ to $F(f'')$ in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Y)$. Unwinding the definitions, this is equivalent to the commutativity of the outer cycle of the diagram
\[ \xymatrix@R =50pt@C=50pt{ & & F(vfu) \ar@ {=>}[dr]^{ \mu _{v'_{11}, (vfu)_{10} } } & & \\ & F(vf) \ar@ {=>}[ur]^{ \mu _{ (vf)_{10}, u_{00}}} \ar@ {=>}[dr]^{ \mu _{v'_{11}, (vf)_{10} } } & & F(v'vfu) \ar@ {=>}[dr]^{ \mu _{ (v'vfu)_{10}, u'_{00} } } & \\ F(f) \ar@ {=>}[ur]^{ \mu _{v_{11}, f_{10} } }\ar@ {=>}[rr]^{ \mu _{ (v'v)_{11}, f_{10} }} & & F(v'vf) \ar@ {=>}[ur]^{ \mu _{ (v'vf)_{10}, u_{00} }} \ar@ {=>}[rr]^{ \mu _{ (v'vf)_{10}, (uu')_{00} }} & & F( v'vfuu') } \]
in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Y)$. In fact, the entire diagram commutes. The commutativity of the upper square follows by applying property $(c)$ of Definition 2.2.4.5 to the composable triple of morphisms
\[ (0,A') \xrightarrow {u_{00} } (0,A) \xrightarrow { (vf)_{10} } (1,B') \xrightarrow { v'_{11} } (1,B'') \]
in the product category $[1] \times \operatorname{\mathcal{A}}$. The commutativity of the lower left triangle follows by applying property $(c)$ to the composable triple of morphisms
\[ (0,A) \xrightarrow {f_{10}} (1,B) \xrightarrow { v_{11} } (1,B') \xrightarrow { v'_{11} } (1,B'') \]
and noting that the composition constraint $\mu _{ v'_{11}, v_{11} }$ is equal to the identity (by virtue of our assumption that the lax functor $U|_{ \{ 1\} \times \operatorname{\mathcal{A}}}$ is constant). Similarly, the commutativity of the lower right triangle follows by applying $(c)$ to the compostable triple of morphisms
\[ (0,A'') \xrightarrow { u'_{00} } (0,A') \xrightarrow {u_{00} } (0,A) \xrightarrow { (v'vf)_{10} } (1,B'') \]
and noting that the composition constraint $\mu _{ u_{00}, u'_{00} }$ is equal to the identity (by virtue of our assumption that the lax functor $U|_{ \{ 0\} \times \operatorname{\mathcal{A}}}$ is constant).
$\square$