record BimonoidalR : Type A *bimonoidal category* is a category with two monoidal structures,
one additive and one multiplicative, that are compatible with each
other in a similar way to elementary algebra.
Totality: total
Visibility: public export
Constructor: MkBimonoidalR : (hom : Hom obj) -> (add : (obj -> obj -> obj)) -> (mul : (obj -> obj -> obj)) -> (zero : obj) -> (one : obj) -> Bimonoidal hom add mul zero one => BimonoidalR
Projections:
.absorbl : (rec : BimonoidalR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
.absorbl' : (rec : BimonoidalR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
.absorbr : (rec : BimonoidalR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
.absorbr' : (rec : BimonoidalR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
.add : ({rec:0} : BimonoidalR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.addCatR : BimonoidalR -> MonoidalR Convert this into a `MonoidalR` with the additive tensor product.
.addR : (rec : BimonoidalR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
.bimonoidalR : BimonoidalR -> BimonoidalR Convert this into a `BimonoidalR`.
.categoryR : BimonoidalR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : BimonoidalR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.distribl : (rec : BimonoidalR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
.distribl' : (rec : BimonoidalR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
.distribr : (rec : BimonoidalR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
.distribr' : (rec : BimonoidalR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
.hom : ({rec:0} : BimonoidalR) -> Hom ({rec:0} .obj).id : (rec : BimonoidalR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : BimonoidalR) -> Bimonoidal ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one).mul : ({rec:0} : BimonoidalR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.mulCatR : BimonoidalR -> MonoidalR Convert this into a `MonoidalR` with the multiplicative tensor product.
.mulR : (rec : BimonoidalR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
0 .obj : BimonoidalR -> Type.one : ({rec:0} : BimonoidalR) -> {rec:0} .obj.zero : ({rec:0} : BimonoidalR) -> {rec:0} .obj
.hom : ({rec:0} : BimonoidalR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .mul : ({rec:0} : BimonoidalR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .add : ({rec:0} : BimonoidalR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .zero : ({rec:0} : BimonoidalR) -> {rec:0} .obj- Totality: total
Visibility: public export .one : ({rec:0} : BimonoidalR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : BimonoidalR) -> Bimonoidal ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one)- Totality: total
Visibility: public export PreBimonoidalR : Type See `PreMonoidal`.
Totality: total
Visibility: public export.categoryR : BimonoidalR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : BimonoidalR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : BimonoidalR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export.addR : (rec : BimonoidalR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.mulR : (rec : BimonoidalR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.addCatR : BimonoidalR -> MonoidalR Convert this into a `MonoidalR` with the additive tensor product.
Totality: total
Visibility: public export.mulCatR : BimonoidalR -> MonoidalR Convert this into a `MonoidalR` with the multiplicative tensor product.
Totality: total
Visibility: public export.bimonoidalR : BimonoidalR -> BimonoidalR Convert this into a `BimonoidalR`.
Totality: total
Visibility: public export.distribl : (rec : BimonoidalR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
Totality: total
Visibility: public export.distribl' : (rec : BimonoidalR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
Totality: total
Visibility: public export.distribr : (rec : BimonoidalR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
Totality: total
Visibility: public export.distribr' : (rec : BimonoidalR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
Totality: total
Visibility: public export.absorbl : (rec : BimonoidalR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
Totality: total
Visibility: public export.absorbl' : (rec : BimonoidalR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
Totality: total
Visibility: public export.absorbr : (rec : BimonoidalR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
Totality: total
Visibility: public export.absorbr' : (rec : BimonoidalR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
Totality: total
Visibility: public exportrecord RigCategoryR : Type A rig category is a bimonoidal category whose additive structure
is symmetric. The name "rig" comes from the algebraic structure
the definition is based on (a ring without negatives).
Totality: total
Visibility: public export
Constructor: MkRigCategoryR : (hom : Hom obj) -> (add : (obj -> obj -> obj)) -> (mul : (obj -> obj -> obj)) -> (zero : obj) -> (one : obj) -> RigCategory hom add mul zero one => RigCategoryR
Projections:
.absorbl : (rec : RigCategoryR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
.absorbl' : (rec : RigCategoryR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
.absorbr : (rec : RigCategoryR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
.absorbr' : (rec : RigCategoryR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
.add : ({rec:0} : RigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.addCatR : RigCategoryR -> SymmetricR Convert this into a `SymmetricR` with the additive tensor product.
.addR : (rec : RigCategoryR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
.bimonoidalR : RigCategoryR -> BimonoidalR Convert this into a `BimonoidalR`.
.categoryR : RigCategoryR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : RigCategoryR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.distribl : (rec : RigCategoryR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
.distribl' : (rec : RigCategoryR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
.distribr : (rec : RigCategoryR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
.distribr' : (rec : RigCategoryR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
.hom : ({rec:0} : RigCategoryR) -> Hom ({rec:0} .obj).id : (rec : RigCategoryR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : RigCategoryR) -> RigCategory ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one).mul : ({rec:0} : RigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.mulCatR : RigCategoryR -> MonoidalR Convert this into a `MonoidalR` with the multiplicative tensor product.
.mulR : (rec : RigCategoryR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
0 .obj : RigCategoryR -> Type.one : ({rec:0} : RigCategoryR) -> {rec:0} .obj.rigCategoryR : RigCategoryR -> RigCategoryR Convert this into a `RigCategoryR`.
.zero : ({rec:0} : RigCategoryR) -> {rec:0} .obj
.hom : ({rec:0} : RigCategoryR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .mul : ({rec:0} : RigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .add : ({rec:0} : RigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .zero : ({rec:0} : RigCategoryR) -> {rec:0} .obj- Totality: total
Visibility: public export .one : ({rec:0} : RigCategoryR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : RigCategoryR) -> RigCategory ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one)- Totality: total
Visibility: public export PreRigCategoryR : Type See `PreMonoidal`.
Totality: total
Visibility: public export.categoryR : RigCategoryR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : RigCategoryR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : RigCategoryR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export.addR : (rec : RigCategoryR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.mulR : (rec : RigCategoryR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.addCatR : RigCategoryR -> SymmetricR Convert this into a `SymmetricR` with the additive tensor product.
Totality: total
Visibility: public export.mulCatR : RigCategoryR -> MonoidalR Convert this into a `MonoidalR` with the multiplicative tensor product.
Totality: total
Visibility: public export.bimonoidalR : RigCategoryR -> BimonoidalR Convert this into a `BimonoidalR`.
Totality: total
Visibility: public export.distribl : (rec : RigCategoryR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
Totality: total
Visibility: public export.distribl' : (rec : RigCategoryR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
Totality: total
Visibility: public export.distribr : (rec : RigCategoryR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
Totality: total
Visibility: public export.distribr' : (rec : RigCategoryR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
Totality: total
Visibility: public export.absorbl : (rec : RigCategoryR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
Totality: total
Visibility: public export.absorbl' : (rec : RigCategoryR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
Totality: total
Visibility: public export.absorbr : (rec : RigCategoryR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
Totality: total
Visibility: public export.absorbr' : (rec : RigCategoryR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
Totality: total
Visibility: public export.rigCategoryR : RigCategoryR -> RigCategoryR Convert this into a `RigCategoryR`.
Totality: total
Visibility: public exportrecord SymRigCategoryR : Type- Totality: total
Visibility: public export
Constructor: MkSymRigCategoryR : (hom : Hom obj) -> (add : (obj -> obj -> obj)) -> (mul : (obj -> obj -> obj)) -> (zero : obj) -> (one : obj) -> SymRigCategory hom add mul zero one => SymRigCategoryR
Projections:
.absorbl : (rec : SymRigCategoryR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
.absorbl' : (rec : SymRigCategoryR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
.absorbr : (rec : SymRigCategoryR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
.absorbr' : (rec : SymRigCategoryR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
.add : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.addCatR : SymRigCategoryR -> SymmetricR Convert this into a `SymmetricR` with the additive tensor product.
.addR : (rec : SymRigCategoryR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
.bimonoidalR : SymRigCategoryR -> BimonoidalR Convert this into a `BimonoidalR`.
.categoryR : SymRigCategoryR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : SymRigCategoryR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.distribl : (rec : SymRigCategoryR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
.distribl' : (rec : SymRigCategoryR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
.distribr : (rec : SymRigCategoryR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
.distribr' : (rec : SymRigCategoryR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
.hom : ({rec:0} : SymRigCategoryR) -> Hom ({rec:0} .obj).id : (rec : SymRigCategoryR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : SymRigCategoryR) -> SymRigCategory ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one).mul : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.mulCatR : SymRigCategoryR -> SymmetricR Convert this into a `SymmetricR` with the multiplicative tensor product.
.mulR : (rec : SymRigCategoryR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
0 .obj : SymRigCategoryR -> Type.one : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj.rigCategoryR : SymRigCategoryR -> RigCategoryR Convert this into a `RigCategoryR`.
.symRigCategoryR : SymRigCategoryR -> SymRigCategoryR Convert this into a `SymRigCategoryR`.
.zero : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj
.hom : ({rec:0} : SymRigCategoryR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .mul : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .add : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .zero : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj- Totality: total
Visibility: public export .one : ({rec:0} : SymRigCategoryR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : SymRigCategoryR) -> SymRigCategory ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one)- Totality: total
Visibility: public export PreSymRigCategoryR : Type- Totality: total
Visibility: public export .categoryR : SymRigCategoryR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : SymRigCategoryR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : SymRigCategoryR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export.addR : (rec : SymRigCategoryR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.mulR : (rec : SymRigCategoryR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.addCatR : SymRigCategoryR -> SymmetricR Convert this into a `SymmetricR` with the additive tensor product.
Totality: total
Visibility: public export.mulCatR : SymRigCategoryR -> SymmetricR Convert this into a `SymmetricR` with the multiplicative tensor product.
Totality: total
Visibility: public export.bimonoidalR : SymRigCategoryR -> BimonoidalR Convert this into a `BimonoidalR`.
Totality: total
Visibility: public export.distribl : (rec : SymRigCategoryR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
Totality: total
Visibility: public export.distribl' : (rec : SymRigCategoryR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
Totality: total
Visibility: public export.distribr : (rec : SymRigCategoryR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
Totality: total
Visibility: public export.distribr' : (rec : SymRigCategoryR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
Totality: total
Visibility: public export.absorbl : (rec : SymRigCategoryR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
Totality: total
Visibility: public export.absorbl' : (rec : SymRigCategoryR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
Totality: total
Visibility: public export.absorbr : (rec : SymRigCategoryR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
Totality: total
Visibility: public export.absorbr' : (rec : SymRigCategoryR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
Totality: total
Visibility: public export.rigCategoryR : SymRigCategoryR -> RigCategoryR Convert this into a `RigCategoryR`.
Totality: total
Visibility: public export.symRigCategoryR : SymRigCategoryR -> SymRigCategoryR Convert this into a `SymRigCategoryR`.
Totality: total
Visibility: public exportrecord DistributiveR : Type- Totality: total
Visibility: public export
Constructor: MkDistributiveR : (hom : Hom obj) -> (add : (obj -> obj -> obj)) -> (mul : (obj -> obj -> obj)) -> (zero : obj) -> (one : obj) -> Distributive hom add mul zero one => DistributiveR
Projections:
.absorbl : (rec : DistributiveR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
.absorbl' : (rec : DistributiveR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
.absorbr : (rec : DistributiveR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
.absorbr' : (rec : DistributiveR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
.add : ({rec:0} : DistributiveR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.addCatR : DistributiveR -> CocartesianR Convert this into a `CocartesianR` with the additive tensor product.
.addR : (rec : DistributiveR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
.bimonoidalR : DistributiveR -> BimonoidalR Convert this into a `BimonoidalR`.
.categoryR : DistributiveR -> CategoryR Convert this into a `CategoryR`.
.comp : (rec : DistributiveR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
.coprod : (rec : DistributiveR) -> rec .hom a b -> rec .hom a' b -> rec .hom (rec .add a a') b The universal property of the coproduct.
.distribl : (rec : DistributiveR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
.distribl' : (rec : DistributiveR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
.distribr : (rec : DistributiveR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
.distribr' : (rec : DistributiveR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
.distributiveR : DistributiveR -> DistributiveR Convert this into a `DistributiveR`.
.elim : (rec : DistributiveR) -> rec .hom a (rec .one) The counit of the universal comonoid structure.
.hom : ({rec:0} : DistributiveR) -> Hom ({rec:0} .obj).id : (rec : DistributiveR) -> rec .hom a a The identity morphism of an object `a`.
.impl : ({rec:0} : DistributiveR) -> Distributive ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one).injl : (rec : DistributiveR) -> rec .hom a (rec .add a b) The left injection of the coproduct.
.injr : (rec : DistributiveR) -> rec .hom b (rec .add a b) The right injection of the coproduct.
.intro : (rec : DistributiveR) -> rec .hom (rec .zero) a The unit of the universal monoid structure.
.merge : (rec : DistributiveR) -> rec .hom (rec .add a a) a The join of the universal monoid structure.
.mul : ({rec:0} : DistributiveR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj.mulCatR : DistributiveR -> CartesianR Convert this into a `CartesianR` with the multiplicative tensor product.
.mulR : (rec : DistributiveR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
0 .obj : DistributiveR -> Type.one : ({rec:0} : DistributiveR) -> {rec:0} .obj.prod : (rec : DistributiveR) -> rec .hom a b -> rec .hom a b' -> rec .hom a (rec .mul b b') The universal property of the product.
.projl : (rec : DistributiveR) -> rec .hom (rec .mul a b) a The left projection of the product.
.projr : (rec : DistributiveR) -> rec .hom (rec .mul a b) b The right projection of the product.
.rigCategoryR : DistributiveR -> RigCategoryR Convert this into a `RigCategoryR`.
.split : (rec : DistributiveR) -> rec .hom a (rec .mul a a) The cojoin of the universal comonoid structure.
.symRigCategoryR : DistributiveR -> SymRigCategoryR Convert this into a `SymRigCategoryR`.
.zero : ({rec:0} : DistributiveR) -> {rec:0} .obj
.hom : ({rec:0} : DistributiveR) -> Hom ({rec:0} .obj)- Totality: total
Visibility: public export .mul : ({rec:0} : DistributiveR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .add : ({rec:0} : DistributiveR) -> {rec:0} .obj -> {rec:0} .obj -> {rec:0} .obj- Totality: total
Visibility: public export .zero : ({rec:0} : DistributiveR) -> {rec:0} .obj- Totality: total
Visibility: public export .one : ({rec:0} : DistributiveR) -> {rec:0} .obj- Totality: total
Visibility: public export .impl : ({rec:0} : DistributiveR) -> Distributive ({rec:0} .hom) ({rec:0} .add) ({rec:0} .mul) ({rec:0} .zero) ({rec:0} .one)- Totality: total
Visibility: public export PreDistributiveR : Type- Totality: total
Visibility: public export .categoryR : DistributiveR -> CategoryR Convert this into a `CategoryR`.
Totality: total
Visibility: public export.id : (rec : DistributiveR) -> rec .hom a a The identity morphism of an object `a`.
Totality: total
Visibility: public export.comp : (rec : DistributiveR) -> rec .hom b c -> rec .hom a b -> rec .hom a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export.addR : (rec : DistributiveR) -> EndoBifunctorR (rec .categoryR) The additive tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.mulR : (rec : DistributiveR) -> EndoBifunctorR (rec .categoryR) The multiplicative tensor product as a `BifunctorR`.
Totality: total
Visibility: public export.addCatR : DistributiveR -> CocartesianR Convert this into a `CocartesianR` with the additive tensor product.
Totality: total
Visibility: public export.mulCatR : DistributiveR -> CartesianR Convert this into a `CartesianR` with the multiplicative tensor product.
Totality: total
Visibility: public export.bimonoidalR : DistributiveR -> BimonoidalR Convert this into a `BimonoidalR`.
Totality: total
Visibility: public export.distribl : (rec : DistributiveR) -> rec .hom (rec .mul a (rec .add b c)) (rec .add (rec .mul a b) (rec .mul a c)) The left distributor.
Totality: total
Visibility: public export.distribl' : (rec : DistributiveR) -> rec .hom (rec .add (rec .mul a b) (rec .mul a c)) (rec .mul a (rec .add b c)) The inverse of `(.distribl)`, the left distributor.
Totality: total
Visibility: public export.distribr : (rec : DistributiveR) -> rec .hom (rec .mul (rec .add a b) c) (rec .add (rec .mul a c) (rec .mul b c)) The right distributor.
Totality: total
Visibility: public export.distribr' : (rec : DistributiveR) -> rec .hom (rec .add (rec .mul a c) (rec .mul b c)) (rec .mul (rec .add a b) c) The inverse of `(.distribr)`, the right distributor.
Totality: total
Visibility: public export.absorbl : (rec : DistributiveR) -> rec .hom (rec .mul a (rec .zero)) (rec .zero) The left absorbor.
Totality: total
Visibility: public export.absorbl' : (rec : DistributiveR) -> rec .hom (rec .zero) (rec .mul a (rec .zero)) The inverse of `(.absorbl)`, the left absorbor.
Totality: total
Visibility: public export.absorbr : (rec : DistributiveR) -> rec .hom (rec .mul (rec .zero) a) (rec .zero) The right absorbor.
Totality: total
Visibility: public export.absorbr' : (rec : DistributiveR) -> rec .hom (rec .zero) (rec .mul (rec .zero) a) The inverse of `(.absorbr)`, the right absorbor.
Totality: total
Visibility: public export.rigCategoryR : DistributiveR -> RigCategoryR Convert this into a `RigCategoryR`.
Totality: total
Visibility: public export.symRigCategoryR : DistributiveR -> SymRigCategoryR Convert this into a `SymRigCategoryR`.
Totality: total
Visibility: public export.distributiveR : DistributiveR -> DistributiveR Convert this into a `DistributiveR`.
Totality: total
Visibility: public export.projl : (rec : DistributiveR) -> rec .hom (rec .mul a b) a The left projection of the product.
Totality: total
Visibility: public export.projr : (rec : DistributiveR) -> rec .hom (rec .mul a b) b The right projection of the product.
Totality: total
Visibility: public export.prod : (rec : DistributiveR) -> rec .hom a b -> rec .hom a b' -> rec .hom a (rec .mul b b') The universal property of the product.
Totality: total
Visibility: public export.split : (rec : DistributiveR) -> rec .hom a (rec .mul a a) The cojoin of the universal comonoid structure.
Totality: total
Visibility: public export.elim : (rec : DistributiveR) -> rec .hom a (rec .one) The counit of the universal comonoid structure.
Totality: total
Visibility: public export.injl : (rec : DistributiveR) -> rec .hom a (rec .add a b) The left injection of the coproduct.
Totality: total
Visibility: public export.injr : (rec : DistributiveR) -> rec .hom b (rec .add a b) The right injection of the coproduct.
Totality: total
Visibility: public export.coprod : (rec : DistributiveR) -> rec .hom a b -> rec .hom a' b -> rec .hom (rec .add a a') b The universal property of the coproduct.
Totality: total
Visibility: public export.merge : (rec : DistributiveR) -> rec .hom (rec .add a a) a The join of the universal monoid structure.
Totality: total
Visibility: public export.intro : (rec : DistributiveR) -> rec .hom (rec .zero) a The unit of the universal monoid structure.
Totality: total
Visibility: public export