\begin{mathpar}
\msem{\mconst} \of \msem{\mG} \xto{\terminalmorphism} \terminal \xto{\msemConst\mconst}
\msem{\constType\mconst}

\msem{\mx} \of \msem\mG = \prod_{\makebox[0pt]{$\scriptstyle x \in
        \Domain \mG$}} \msem{\mG(x)} \xto{\proj{\mx}}
\msem{\mG(\mx)}

\msem{\unitval} \of \msem{\mG} \xto{\terminalmorphism} \terminal

\msem{\vpair{\mV_1}{\mV_2}} \of \msem{\mG}
\xto{\prodmorphism{\msem{\mV_1}}{\msem{\mV_2}}}
\msem{\mA_1}\times\msem{\mA_2}

\msem{\inject{\indx i}\mValue} \of \msem{\mG} \xto{\msem\mValue}
\msem{\mA_{\indx i}}\xto{\inj{\indx i}}
\msem{\mA_1} + \msem{\mA_2}

\msem{\thunk \mM} \of \msem{\mG} \xto{\msem\mM} \carrier{\msem{\mB}}

\DELTA{
  \msem{\coerce\mM} \of
  \msem{\mG} \xto{\msem\mM}
  \Monad_{\e_1} \msem{\mA}
  \xto{\MonadMorphism_{\e_1\subset\e_2}}
  \Monad_{\e_2}\msem{\mA}
}

%\G \cinf[\e_1] \mM \of \sF[\e_1]\mA
%\G \cinf[\e_2] \coerce\mM \of \sF[\e_2]\mA

\msem{\return[\DELTA{\scriptstyle\e}] \mValue} \of \msem{\mG} \xto{\mValue} \msem{\mA}
\xto{\unit_{\DELTA{\scriptscriptstyle\e}}} \carrier{\F\msem{\mA}}

\msem{\sbind \mM\mx\mA\mN} \of \msem\mG
\xto{\prodmorphism\id{\msem\mM}}
\msem{\mG}\times\Monad\msem{\mA}
\xto{\lifting{\msem{\mN}}}
\carrier{\msem{\mB}}

\msem{\cpair{\mM_1}{\mM_2}} \of \msem{\mG}
\xto{
  \prodmorphism{\msem{\mM_1}}{\msem{\mM_2}}
}
\carrier{\msem{\mB_1}}\times\carrier{\msem{\mB_2}}

\msem{\apply{\indx i}\mM} \of \msem{\mG}
\xto{\msem{\mM}}
\carrier{\msem{\mB_1}}\times\carrier{\msem{\mB_2}}
\xto{\proj{\indx i}}
\carrier{\msem{\mB_{\indx i}}}

\msem{\abst\mx\mA\mM} \of \msem{\mG} \xto{
  \ilam{\msem{\mA}}{\msem{\mM}}
}
\carrier{\msem{\mB}}^{\msem{\mA}}

\msem{\apply\mValue\mM} \of \msem{\mG}
\xto{\prodmorphism{\msem\mM}{\msem{\mValue}}}
\carrier{\msem{\mB}}^{\msem{\mA}}\times\msem{\mA}
\xto{\eval}
\carrier{\msem{\mB}}


\msem{\prodmatch \mValue{\mx_1}{\mA_1}{\mx_2}{\mA_2}\mM}
\of \msem{\mG}\xto{\prodmorphism{\id}{\mValue}}
\msem{\mG}\times\msem{\mA_1}\times\msem{\mA_2}
\xto{\msem{\mM}}
\carrier{\msem{\mB}}

\msem{\zeromatch\mValue\mB} \of
\msem{\mG} \xto{\msem{\mValue}} \initial \xto{\initialmorphism} \carrier{\msem{\mB}}

{\begin{aligned}
&\msem{\plusmatch \mValue{\mx_1}{\mA_1}{\mM_1}{\mx_2}{\mA_2}{\mM_2}}
\of
\msem{\mG} \xto{\prodmorphism\id{\msem{\mValue}}}
\msem{\mG}\times(\msem{\mA_1}+\msem{\mA_2})
\\&\qquad\qquad\qquad\smash{\explain*\isomorphic{distributivity}}
(\msem\mG\times\msem{\mA_1})+
(\msem\mG\times\msem{\mA_2})
\xto{\coprodmorphism{\msem{\mM_1}}
                    {\msem{\mM_2}}}
\carrier{\msem{\mB}}
\end{aligned}
}


\msem{\force \mValue} \of \msem{\mG} \xto{\msem{\mValue}} \carrier{\msem{\mB}}

\msem{\mop_{\mValue}^{\mB}\mM } \of
\msem{\mG} \xto{\prodmorphism{\id}{\msem\mValue}}
\msem{\mG}\times\msem{\sParam}
\xto{\id\times\genopsem[]\mop}
\msem{\mG}\times\Monad\msem\sArity
\xto{\lifting{\msem{\mM}}}
\carrier{\msem{\mB}}

%% \sarity{\sArity}{\sParam}}, \mop \in \Opset]{
%%   \G \cinf \mV \of \sParam \quad
%%   \G \cinf \mM \of \funtype{\sArity}\mB

%%   \G \cinf \of \mB
\end{mathpar}
