群対象

summary.icon

WIP.icon

code: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.icon