余クライスリ評価関手の余クライスリ結合

モノイド圏 本編ネタ

\newcommand{\Arr}{\:\downarrow } % \newcommand{\coM}{\boldsymbol{d} } % comultiplication \newcommand{\coU}{\boldsymbol{e} } % counit \newcommand{\Ev}{\mathrm{Ev} } \newcommand{\gcoM}{\bar{\boldsymbol{\delta}} } % generic comultiplication \newcommand{\oast}{\circledast }
評価双関手の交替律（エレベーター法則）

t[\vec{f}] ; \beta[\vec{B}] = \beta[\vec{A}] ; t'[\vec{f}]

行列形式表記では：

\begin{bmatrix} t[\vec{A}] \\ t[\vec{f}] \Arr\\ t[\vec{B}] \\ \beta[\vec{B}] \Arr\\ t'[\vec{B}] \end{bmatrix} = \begin{bmatrix} t[\vec{A}] \\ \beta[\vec{A}] \Arr\\ t'[\vec{A}] \\ t'[\vec{f}] \Arr\\ t'[\vec{B}] \end{bmatrix}

評価関手：

\widehat{\Ev}( (t, \beta, t'), \vec{A})\hat{;}\widehat{\Ev}( (t', \beta', t''), \vec{A}) =\\ \begin{array}{c} \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}]) \end{bmatrix} \\ F \begin{bmatrix} F(t[\vec{A}])\\ \gcoM_t^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast( F\oast \vec{A}) } ] \Arr\\ t[\vec{A}]\\ \beta[\vec{A}] \Arr\\ t'[\vec{A}] \end{bmatrix} \\ \begin{bmatrix} F(t'[\vec{A}]) \\ \gcoM_{t'}^{\vec{A}} \Arr\\ t'[F\oast \vec{A}] \\ t'[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t'[\vec{A}]\\ \beta'[\vec{A}] \Arr\\ t''[\vec{A}] \end{bmatrix} \end{array}

新しいターゲット（目的の等式）：

\begin{bmatrix} F(t[\vec{A}]) \\ \gcoM_t^\vec{A} \Arr\\ t[F\oast \vec{A}]\\ \coU_{t[F\oast \vec{A}]} \Arr\\ t[\vec{A}]\\ \end{bmatrix} = \begin{bmatrix} F(t[\vec{A}]) \\ \coM_{t[\vec{A}]} \Arr\\ F^2(t[\vec{A}])\\ F(\gcoM_t^{\vec{A}} )\Arr\\ F(t[F\oast \vec{A}] )\\ F(t[\coU_{\oast( F\oast \vec{A}) } ] )\Arr\\ F(t[\vec{A}] )\\ \gcoM_{t}^{\vec{A}} \Arr\\ t[F\oast \vec{A}] \\ t[\coU_{\oast (F\oast \vec{A})} ] \Arr\\ t[\vec{A}] \\ \end{bmatrix}