\renewcommand\e{\DELTA{\scriptstyle\epsilon}}
\begin{mathpar}
  \msemValTerm\mc(\mg) \definedby \msem\mc \quad
  \msemValTerm\mx(\mg) \definedby \projection_{\mx}(\mg) \quad
  \msemValTerm\unitval(\mg) \definedby \star
  \\
  \msemValTerm{\vpair{\mV_1}{\mV_2}}(\mg) \definedby
  \prodmorphism{\msem{\mV_1}(\mg)}{\msem{\mV_2}(\mg)}
  \\
  \msemValTerm{\inject{\indx i}\mV}(\mg) \definedby
  \injection_i(\msem{\mV}(\mg))
\unignore{\\}
\DELTA{\ensuremath{  \msemCompTerm[\e_2]{\coerce\mM}(\mg) \definedby
  \MonadMorphism_{\e_1\subset\e_2}(\msem\mM(\mg))}}
  \\
  \msemCompTerm{\return\mV}(\mg) \definedby
  \unit_{\e}(\msem\mV(\mg))
  \\
  \msemCompTerm{\sbind \mM\mx\mA\mN}(\mg) \definedby
  \MonadicBind{\msem\mM(\mg)}{\parent{\lam{\ta}{\msem\mN(\singleExtend{\mg}{\mx}{\ta})}}}
  \\
  \msemCompTerm{\apply{\indx i}\mM}(\mg) \definedby
  \projection_i(\msem\mM(\mg))
  \\
  \msemCompTerm{\apply\mV\mM}(\mg) \definedby
  \parent{\msem{\mM}(\mg)}(\msem\mV(\mg))
  \\
  \msemCompTerm{\zeromatch\mV\mB} \definedby \initialmorphism_{\msem{\mB}}
  \\
  \msemCompTerm{\plusmatch
    \mV{\mx_1}{\mA_1}{\mM_1}{\mx_2}{\mA_2}{\mM_2}}(\mg)
  \mspace{80mu}\\\mspace{140mu}
  \definedby
  \begin{cases}
    \msem{\mM_1}(\singleExtend\mg{\mx_1}{\ta_1}) &
    \msem\mV(\mg) = \injection_1\ta_1 \\
    \msem{\mM_2}(\singleExtend\mg{\mx_2}{\ta_2}) &
    \msem\mV(\mg) = \injection_2\ta_2
  \end{cases}
  %% \msemCompTerm{\sfix \mx{\mB}\mM}(\mg) \definedby \fix
  %% {\tabst{f\in\carrier{\msem\mB}}{\msem{\mM}(\singleExtend\mg{\mx}{f})}}
  \\
  \msemCompTerm{\mop_{\mV}^{\mB}\mM}(\mg) \definedby \MonadicBind{\genopsem\mop(\msem\mV(\mg))}{\parent{\msem\mM(\mg)}}
\end{mathpar}
