Category instances for Semiring
, Ring
, CommSemiring
, and CommRing
. #
We introduce the bundled categories:
SemiRingCat
RingCat
CommSemiRingCat
CommRingCat
along with the relevant forgetful functors between them.
An alias for Semiring.{max u v}
, to deal around unification issues.
Instances For
RingHom
doesn't actually assume associativity. This alias is needed to make the category
theory machinery work. We use the same trick in MonCat.AssocMonoidHom
.
Instances For
Construct a bundled SemiRing from the underlying type and typeclass.
Instances For
Typecheck a RingHom
as a morphism in SemiRingCat
.
Instances For
Typecheck a RingHom
as a morphism in RingCat
.
Instances For
Construct a bundled CommSemiRingCat
from the underlying type and typeclass.
Instances For
Typecheck a RingHom
as a morphism in CommSemiRingCat
.
Instances For
The forgetful functor from commutative rings to (multiplicative) commutative monoids.
Ring equivalence are isomorphisms in category of commutative semirings
Instances For
Construct a bundled CommRingCat
from the underlying type and typeclass.
Instances For
Typecheck a RingHom
as a morphism in CommRingCat
.
Instances For
The forgetful functor from commutative rings to (multiplicative) commutative monoids.
Build an isomorphism in the category RingCat
from a RingEquiv
between RingCat
s.
Instances For
Build an isomorphism in the category CommRingCat
from a RingEquiv
between CommRingCat
s.
Instances For
Build a RingEquiv
from an isomorphism in the category CommRingCat
.
Instances For
Ring equivalences between RingCat
s are the same as (isomorphic to) isomorphisms in
RingCat
.
Instances For
Ring equivalences between CommRingCat
s are the same as (isomorphic to) isomorphisms
in CommRingCat
.