\alpha_{(B,Y),A}\:{\ensuremath{\mathpzc{A}}\xspace}\left({K(B,Y)},\hspace{1\horspace}{A}\right)\to F((B,Y),A)
1\xrightarrow[]{\operatorname{id}_{B}} {\ensuremath{\mathpzc{A}}\xspace}\left({B},\hspace{1\horspace}{B}\right)\xrightarrow[]{\alpha_{(B,Y),B}}F((B,Y),B)
\alpha_{(B,Y),A}\:{\ensuremath{\mathpzc{A}}\xspace}\left({K(B,Y)},\hspace{1\horspace}{A}\right)\to F((B,Y),A)
Cd. *
Cd. [#3][#4] ##1#2p#9l&##2#9r#2l
##3#9d#2o&##4
[3.8][9]A(A,A)F((A,M(u)(Y)),A)A(B,A)F((B,Y),A)_(A,M(u)(Y)),A-uF((u,id_),A)_(B,Y),A So, in order to reach the bijection we want, we define
\alpha_{(B,Y),A}(u)\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} F((u,\operatorname{id}_{}),A)\left(\eta_{(A,M(u)(Y))}\right).
Given \theta\:u
\ext@arrow 0055{\Rightarrowfill@}{}{} v\:B\to A in \ensuremath{\mathpzc{A}}\xspace, considering
\underline{\theta}^{Y}\:(u,M(\theta)_Y)
\ext@arrow 0055{\Rightarrowfill@}{}{}(v,\operatorname{id}_{})\:(B,Y)\to (A,M(v)(Y))
and using that \alpha_{(v,\operatorname{id}_{}),A}=\operatorname{id}_{}, we will have by the 2-dimensional axiom of cartesian-marked oplax naturality that
\alpha_{(B,Y),A}(\theta)=F(\underline{\theta}^Y,A)_{\hspace{1.0\horspace}\alpha_{(A,M(v)(Y)),A}(\operatorname{id}_{A})}\circ {\left(\alpha_{(u,M(\theta)_Y),A}\right)}_{\operatorname{id}_{A}}
So we firstly define the components of the structure 2-cells that express the cartesian-marked oplax naturality of \alpha_{(B,Y),A} in (B,Y) and then we will read how to define the action of \alpha_{(B,Y),A} on morphisms \theta.
Looking at the diagram of equation (?) applied to (\operatorname{id}_{B},\gamma)\:(B,Y)\to (B,Y') in \ensuremath{\int\ensuremath{^{\operatorname{op}}} \hspace{-0.35ex} M}, we see that, in order to have a bijection between the \alpha’s and the \eta’s, we need to define
{\left(\alpha_{(\operatorname{id}_{B},\gamma),B}\right)}_{\operatorname{id}_{B}}\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} \eta_{(\operatorname{id}_{B},\gamma)}.
Whence, given arbitrary (g,\gamma)\:(B,Y)\to (B',Y') in \ensuremath{\int\ensuremath{^{\operatorname{op}}} \hspace{-0.35ex} M} and w\:B'\to A in \ensuremath{\mathpzc{A}}\xspace, since
(w,\operatorname{id}_{})\circ (g,\gamma)=(\operatorname{id}_{A},M(w)(\gamma))\circ (w\circ g,\operatorname{id}_{}),
we need to define
{\left(\alpha_{(g,\gamma),A}\right)}_w\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} F((w\circ g,\operatorname{id}_{}),A)\left(\eta_{(\operatorname{id}_{A},M(w)(\gamma))}\right).
And at this point we define, by the argument above,
\alpha_{(B,Y),A}(\theta)\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} F(\underline{\theta}^Y,A)_{\eta_{(A,M(v)(Y))}}\circ F((u,\operatorname{id}_{}),A)\left(\eta_{(\operatorname{id}_{A},M(\theta)_Y)}\right)
for every \theta\:u
\ext@arrow 0055{\Rightarrowfill@}{}{}v\:B\to A in \ensuremath{\mathpzc{A}}\xspace.
Looking at the diagram of equation (?) applied to (g,\operatorname{id}_{})\:(B,Y)\to (B',M(g)(Y)) in \ensuremath{\int\ensuremath{^{\operatorname{op}}} \hspace{-0.35ex} M}, we see that, in order to have the bijection we want, we need to define
{\left(\alpha_{(B,Y),g}\right)}_{\operatorname{id}_{B}}\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} \eta_{(g,\operatorname{id}_{})}.
Whence, given an arbitrary f\:A\to A' in \ensuremath{\mathpzc{A}}\xspace and u\:K(B,Y)\to A in \ensuremath{\mathpzc{A}}\xspace, by the compatibility axiom of \operatorname{oplax^{cart}}\mbox{-}\operatorname{lax} applied to (u,\operatorname{id}_{})\:(B,Y)\to (A,M(u)(Y)) in \ensuremath{\int\ensuremath{^{\operatorname{op}}} \hspace{-0.35ex} M} and f\:A\to A' in \ensuremath{\mathpzc{A}}\xspace, we need to define
{\left(\alpha_{(B,Y),f}\right)}_u\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} F((u,\operatorname{id}_{}),A')\left(\eta_{(f,\operatorname{id}_{})}\right).
Now, we verify that such assignments work. To show that \alpha_{(B,Y),A} is a functor, consider u
\ext@arrow 0055{\Rightarrowfill@}{}{\theta} v
\ext@arrow 0055{\Rightarrowfill@}{}{\rho}w\:B\to A in \ensuremath{\mathpzc{A}}\xspace. Then
\alpha_{(B,Y),A}(\rho\circ \theta)\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} F(\underline{(\rho\circ \theta)}^Y,A)_{\eta_{(A,M(w)(Y))}}\circ F((u,\operatorname{id}_{}),A)\left(\eta_{(\operatorname{id}_{A},M(\rho\circ\theta)_Y)}\right)
while \alpha_{(B,Y),A}(\rho)\circ\alpha_{(B,Y),A}(\theta) is equal to
\scalebox{0.935}{$F(\underline{\rho}^Y,A)_{\eta_{(A,M(w)(Y))}}\circ F((v,\operatorname{id}_{}),A)\left(\eta_{(\operatorname{id}_{A},M(\rho)_Y)}\right)\circ F(\underline{\theta}^Y,A)_{\eta_{(A,M(v)(Y))}}\circ F((u,\operatorname{id}_{}),A)\left(\eta_{(\operatorname{id}_{A},M(\theta)_Y)}\right)$}
By the extraordinary naturality of \eta,
\eta_{(\operatorname{id}_{A},M(\rho\circ \theta)_Y)}=F((\operatorname{id}_{A},M(\theta)_Y),A)\left(\eta_{(\operatorname{id}_{A},M(\rho)_Y)}\right)\circ \eta_{(\operatorname{id}_{A},M(\theta)_Y)}
And by the uniqueness of the liftings of 2-cells through \mathcal{G}\mkern-1.4mu\left(M\right), we have that
\underline{(\rho\circ \theta)}^Y=\underline{\rho}^Y\circ (\operatorname{id}_{A},M(\rho)_Y)\hspace{1.0\horspace} \underline{\theta}^Y.
So, by 2-functoriality of F, it suffices to prove that
F(\underline{\theta}^Y,A)_{F((\operatorname{id}_{A},M(\rho)_Y),A)\left(\eta_{(A,M(w)_Y)}\right)}\circ F((u,M(\theta)_Y),A)\left(\eta_{(\operatorname{id}_{A},M(\rho)_Y)}\right)
is equal to
F((v,\operatorname{id}_{}),A)\left(\eta_{(\operatorname{id}_{A},M(\rho)_Y)}\right)\circ F(\underline{\theta}^Y,A)_{\eta_{(A,M(v)(Y))}}.
And this is true by naturality of F(\underline{\theta}^Y,A). The fact that {\left(\alpha_{(B,Y),f}\right)}_u is a natural transformation is checked with techniques similar to the above ones, noticing that \underline{(f\hspace{1.0\horspace}\theta)}^Y=(f,\operatorname{id}_{})\hspace{1.0\horspace}\underline{\theta}^Y. Whereas showing that {\left(\alpha_{(g,\gamma),A}\right)}_w is a natural transformation uses that for (g,\gamma)\:(B,Y)\to (B',Y')
\underline{(\theta\hspace{1.0\horspace} g)}^{Y}=\underline{\theta}^{M(g)(Y)}\hspace{1.0\horspace} (g,\operatorname{id}_{})\quad \text{and}\quad \underline{\theta}^{Y'}\hspace{1.0\horspace}(\operatorname{id}_{},\gamma)=(\operatorname{id}_{},M(v)(\gamma))\hspace{1.5\horspace}\underline{\theta}^{M(g)(Y)}.
At this point, it is straightforward to check that \alpha_{(B,Y),A} is \operatorname{oplax^{cart}}\mbox{-}\operatorname{lax} in ((B,Y),A). And we immediately see that we obtain a bijection between the \alpha’s and the \eta’s.
We extend such bijection to an isomorphism of categories. We send a modification
\Theta_{(B,Y),A}\:\alpha_{(B,Y),A}
\ext@arrow 0055{\Rightarrowfill@}{}{}\beta_{(B,Y),A}\:{\ensuremath{\mathpzc{A}}\xspace}\left({K(B,Y)},\hspace{1\horspace}{A}\right)\to F((B,Y),A)
between \operatorname{oplax^{cart}}\mbox{-}\operatorname{lax} natural transformations in ((B,Y),A) to the modification
Cd (2.5). [6.5] 1 &[-1ex]A(B,B)&F((B,Y),B)
between extraordinary lax natural transformations. We then send a modification
\Gamma_{(B,Y)}\:\eta_{(B,Y)}
\ext@arrow 0055{\Rightarrowfill@}{}{}{\eta'}_{(B,Y)}\:1\to F((B,Y),B)
between extraordinary lax natural transformations to the modification \Theta between \operatorname{oplax^{cart}}\mbox{-}\operatorname{lax} natural transformations such that for every u\:B\to A in \ensuremath{\mathpzc{A}}\xspace
{\left(\Theta_{(B,Y),A}\right)}_{u}\mathrel{\mathrel{\mathop:}\mkern-1.2mu=} F((u,\operatorname{id}_{}),A)\left(\Gamma_{(A,M(u)(Y))}\right).
The two assignments are clearly functorial and inverses of each other.