モノイド対象 - 雑多な感じ

モノイド対象

code:MonoidObject.sig

1-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 -> c

summary.icon

definition.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

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

https://gyazo.com/7da022a582b562eaea8a844e246f0994

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

https://gyazo.com/87a074f7dce013aa508f7441905d9564