可逆律や交換律のポイントフリー化
from モノイド対象
モノイド対象\left\lang\mathrm{ Monoid }\colon c;m ,i \right\rang
in モノイダル圏 \left\lang\mathrm{ MonCAT }\colon C; M=(⊗), I; \alpha, \lambda, \rho \right\rang
(m\otimes c^\wedge); m = \alpha_{c,c,c}; (c^\wedge\otimes m) ;m
\colon (c\otimes c)\otimes c\to c
i.e.
\forall x,y,z \colon c, \: ……
(i\otimes c^\wedge); m = \lambda_c
\colon I\otimes c \to c
(c^\wedge \otimes i) ; m = \rho_c
\colon c\otimes I \to c
組紐持ってこないとダメか
対称モノイド対象\left\lang\mathrm{ SymMonoid }\colon c;m ,i \right\rang
in 対称モノイダル圏 \left\lang\mathrm{ SymMonCAT }\colon C; M=(⊗), I; α, λ, ρ, σ \right\rang
m =