モノイド対象
MonoidObject.sig1-signature <Monoid: c; m, i>
in <MonCAT: C; ⊗, I; α, λ, ρ>
Data
0-morph underlying @ c : C
1-morph product @ m : c ⊗ c -> c
1-morph unit @ i : I -> c
Axioms
2-eq associative
: (m ⊗ c^) ; m == (c,c,c).α ; (c^ ⊗ m) ; m
: (c ⊗ c) ⊗ c -> c
2-eq l-unital
: (i ⊗ c^) ; m == c.λ
: I ⊗ c -> c
2-eq r-unital
: (c^ ⊗ i) ; m == c.ρ
: c ⊗ I -> cin モノイダル圏 \left\lang\mathrm{ MonCAT }\colon C; M=(⊗), I; \alpha, \lambda, \rho \right\rang
0-morph
対象c \colon C
1-morph
演算 multiplication
m\colon c\otimes c \to c
単位元 unit
i\colon I \to c
公理系
(m\otimes c^\wedge); m = \alpha_{c,c,c}; (c^\wedge\otimes m) ;m
\colon (c\otimes c)\otimes c\to 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
