Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid. #
We introduce the bundled categories:
MonCat
AddMonCat
CommMonCat
AddCommMonCat
along with the relevant forgetful functors between them.
AddMonoidHom
doesn't actually assume associativity. This alias is needed to make
the category theory machinery work.
Instances For
Typecheck an AddMonoidHom
as a morphism in AddMonCat
.
Instances For
The category of additive commutative monoids and monoid morphisms.
Instances For
The category of commutative monoids and monoid morphisms.
Instances For
Construct a bundled AddCommMon
from the underlying type and typeclass.
Instances For
Construct a bundled CommMonCat
from the underlying type and typeclass.
Instances For
Typecheck an AddMonoidHom
as a morphism in AddCommMonCat
.
Instances For
Typecheck a MonoidHom
as a morphism in CommMonCat
.
Instances For
Build an isomorphism in the category AddCommMonCat
from an AddEquiv
between AddCommMonoid
s.
Instances For
Build an isomorphism in the category CommMonCat
from a MulEquiv
between CommMonoid
s.
Instances For
Build an AddEquiv
from an isomorphism in the category
AddCommMonCat
.
Instances For
Build a MulEquiv
from an isomorphism in the category CommMonCat
.
Instances For
additive equivalences between AddMonoid
s are the same
as (isomorphic to) isomorphisms in AddMonCat
Instances For
additive equivalences between AddCommMonoid
s are
the same as (isomorphic to) isomorphisms in AddCommMonCat
Instances For
multiplicative equivalences between CommMonoid
s are the same as (isomorphic to) isomorphisms
in CommMonCat