https://arxiv.org/pdf/1311.7642 の2.1 のクライスリ構造〈クライスリ拡張構造〉$`\newcommand{\T}[1]{\text{#1}}
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\PiTy}{\leadsto}
\newcommand{\LL}{\big\langle}
\newcommand{\LR}{\big\rangle}
\newcommand{\hyp}{\text{－} } % used
\require{color} % Using
\newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name
\newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression
\newcommand{\T}[1]{\text{#1} }
`$
$`\leadsto`$ はパイ型の中置二項演算子記号。
$`\T{using }{\bf 2CAT}, {\bf CAT}\\
\T{using } |\hyp|, (\hyp \subseteq \hyp) \\
\T{using } \LL \hyp \to \hyp \LR_\hyp, \LL \hyp \overset{\sim}{\twoto} \hyp : \hyp \to \hyp \LR_\hyp\\
\T{using } (\hyp * \hyp)\\
\T{signature } \NN{KleisliStructData}\: \{\\
\quad \NX{\cat{K}} \in |{\bf 2CAT}|\\
\quad \NX{\cat{A}} \in |{\bf 2CAT}|\\
\quad \T{inclusion } \cat{A} \subseteq \cat{K} \In {\bf 2CAT}\\
\quad \NX{P} \in \LL \cat{A} \to \cat{K} \LR_{\bf CAT}\\
\quad \NX{y} \in (a\in |\cat{A}|) \PiTy \LL a \to P(a) \LR_\cat{K} \\
\quad \NX{\mrm{ext}} \in (a, b\in |\cat{A}|) \ltimes (f \in \LL a \to P(b) \LR_{\cat{K}} )\\
\quad \PiTy
\LL P(a) \to P(b) \LR_{\cat{K}}\\
\quad \T{notation }\NX{\hyp^\#} := \mrm{ext}(\hyp) \\
\quad \NX{\eta} \in (a, b\in |\cat{A}|)\ltimes(f \in \LL a \to P(a)\LR_{\cat{K}}) \\
\quad \PiTy \LL f \overset{\sim}{\twoto} y_a * f^\# : a \to P(a) \LR_{\cat{K}} \\
\quad \NX{\kappa} \in (a \in |\cat{A}|) \PiTy \LL (y_a)^\# \overset{\sim}{\twoto}
\mrm{ID}_{P(a)} : P(a) \to P(a) \LR_{\cat{K}}\\
\quad \T{overload }\\
\quad \NX{\kappa} \in
(a, b, c \in |\cat{A}|) \ltimes (f\in \LL a \to P(a)\LR_{\cat{K}}) \ltimes
( g \in \LL b \to P(c)\LR_{\cat{K}})\\
\quad \PiTy
\LL (f * g^\#)^\# \overset{\sim}{\twoto} f^\# * g^\# : P(a) \to P(c)\LR_{\cat{K}}
\\ \}
`$
