Proposition 2.2.6.6. Let $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ be $2$-categories, and let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a lax functor which is an isomorphism in the category $\operatorname{2Cat}_{\operatorname{Lax}}$. Then $F$ is a functor.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. We will show that, for every pair of composable $1$-morphisms $X \xrightarrow {f} Y \xrightarrow {g} Z$ in the $2$-category $\operatorname{\mathcal{C}}$, the composition constraint $\mu ^{F}_{g,f}: F(g) \circ F(f) \Rightarrow F(g \circ f)$ is an isomorphism (in the ordinary category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{D}}}( F(X), F(Z) )$); the analogous statement for the identity constraints $\epsilon _{X}^{F}: \operatorname{id}_{F(X)} \Rightarrow F(\operatorname{id}_ X)$ follows by a similar (but easier) argument.
Let $G: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be a lax functor which is an inverse of $F$ in the category $\operatorname{2Cat}_{\operatorname{Lax}}$. For any pair of composable $1$-morphisms $X' \xrightarrow {f'} Y' \xrightarrow {g'} Z'$ in the $2$-category $\operatorname{\mathcal{D}}$, the composition constraint $\mu ^{F \circ G}_{g',f'}$ for the lax functor $F \circ G$ is given by the vertical composition
\[ (F \circ G)(g') \circ (F \circ G)(f') \xRightarrow { \mu ^{F}_{G(g'),G(f')} } F( G(g') \circ G(f') ) \xRightarrow {F(\mu ^{G}_{g',f'} )} (F \circ G)(g' \circ f'). \]
Since $F \circ G$ coincides with $\operatorname{id}_{\operatorname{\mathcal{D}}}$ as a lax functor, this composition is the identity $2$-morphism from $g' \circ f'$ to itself. In particular, we see that $F( \mu ^{G}_{g',f'} )$ has a right inverse in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{D}}}( X', Z' )$. It follows that $\mu ^{G}_{g',f'} = G( F(\mu ^{G}_{g',f'} ) )$ has a right inverse in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( G(X'), G(Z') )$.
Applying the same argument with the roles of $F$ and $G$ reversed, we see that the composition constraint $\mu ^{G \circ F}_{g,f} = \operatorname{id}_{g \circ f}$ factors as a vertical composition
\[ (G \circ F)(g) \circ (G \circ F)(f) \xRightarrow { \mu ^{G}_{F(g),F(f)} } G( F(g) \circ F(f) ) \xRightarrow {G(\mu ^{F}_{g,f} )} (G \circ F)(g \circ f). \]
In particular, this shows that $\mu ^{G}_{F(g), F(f)}$ has a left inverse (in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Z)$). Applying the preceding argument in the case $g' = F(g)$ and $f' = F(f)$, we see that $\mu ^{G}_{F(g), F(f)}$ also has a right inverse. It follows that $\mu ^{G}_{F(g), F(f)}$ is an isomorphism in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(X,Z)$. Since $G( \mu ^{F}_{g,f} )$ is a left inverse of $\mu ^{G}_{F(g), F(f)}$, it must also be an isomorphism. It follows that $F( G( \mu ^{F}_{g,f} ) ) = \mu ^{F}_{g,f}$ is an isomorphism in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{D}}}( F(X), F(Z) )$, as desired. $\square$