generated at
群対象

summary
一般のモノイダル圏における

WIP
sig
1-signature <Group: c; m, i, inv> = <Monoid: c; m, i> <+Inverse: ; inv> in <MonCAT: C; ⊗, I; α, λ, ρ> 1- Data 1-morph inv : c -> c Axioms 2-eq l-invertible : Δ ; (inv ⊗ c^) ; m == i : I ⊗ c → c 2-eq r-invertible : (c^ ⊗ i) ; m ⇒ c.ρ : c ⊗ I → c
definition