テレオロジー圏の公理

$`\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\B}[1]{ \{\!| #1 |\!\} }
\newcommand{\A}[2]{ \langle\!| #1 \mid #2 |\!\rangle }
`$

$`\text{Basic} :::\\
\forall A \in |\cat{D}|.\\
\forall M \in |\cat{M}|.\\
\quad A \B{M} = {_A \A{M}{M} }
`$


$`\text{Vanishing} :::\\
\quad \B{I, \varepsilon} = \boldsymbol{\rho} J
`$


$`\text{Bundling} :::\\
\forall M, N\in |\cat{M}|.\\
\quad \B{ M\otimes N , \varepsilon}
=
\begin{pmatrix}
\boldsymbol{\alpha}_{M, N} J\\
\B{M} \B{ N, \varepsilon}\\
\B{ M, \varepsilon}\\
\end{pmatrix}
`$


$`\text{Tightening} :::\\
\forall M\in |\cat{M}|.\\
\forall f:A \to B \In \cat{D}.\\
\quad \begin{pmatrix}
f \B{M} J\\
B\B{M\ \varepsilon}
\end{pmatrix}
=
\begin{pmatrix}
A \B{M} J\\
A \B{M\, \varepsilon}\\
f J
\end{pmatrix}
`$


$`\text{Sliding} ::: \\
\forall A \in |\cat{D}|.\\
\forall v:M \to N \In \cat{M}.\\
\quad \begin{pmatrix}
{_A \A{v}{N} }\\
\B{N, \varepsilon}\\
\end{pmatrix}
=
\begin{pmatrix}
{_A \A{M}{v} }\\
\B{M, \varepsilon}\\
\end{pmatrix}
`$