可逆律や交換律のポイントフリー化

summary.icon

結合律や単位律はポイントフリーにできる

モノイド対象から群対象に行くときに困った

モノイド対象$ \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, \: ……

dragoon8192.iconそもそもポイントフリー以外で書けん！

$ (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 =