Control.Category.Bimonoidal

Definitions

interface Bimonoidal : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> 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.
  
  This is the interface-style definition of a bimonoidal category.
  For the record-style definition, see `Control.Category.Records.BimonoidalR`.
  
  As for coherence laws: they do exist, but they are so numerous as
  to be impractical to write here. (You wouldn't check them anyway.)
  If you do wish to be fully rigorous, here's a textbook on
  bimonoidal categories to read:
  * https://nilesjohnson.net/En-monoidal.html

Parameters: cat, add, mul, z, i
Constraints: Monoidal cat add z, Monoidal cat mul i
Constructor: 

MkBimonoidal

Methods:

distribl : cat (mul a (add b c)) (add (mul a b) (mul a c))

  The left distributor.

distribl' : cat (add (mul a b) (mul a c)) (mul a (add b c))

  The inverse of `distribl`, the left distributor.

distribr : cat (mul (add a b) c) (add (mul a c) (mul b c))

  The right distributor.

distribr' : cat (add (mul a c) (mul b c)) (mul (add a b) c)

  The inverse of `distribr`, the right distributor.

absorbl : cat (mul a z) z

  The left absorbor.

absorbl' : cat z (mul a z)

  The inverse of `absorbl`, the left absorbor.

absorbr : cat (mul z a) z

  The right absorbor.

absorbr' : cat z (mul z a)

  The inverse of `absorbr`, the right absorbor.

Implementations:

Bimonoidal Morphism Either Pair Void ()

Monad m => Bimonoidal (Kleislimorphism m) Either Pair Void ()

distribl : Bimonoidal cat add mul z i => cat (mul a (add b c)) (add (mul a b) (mul a c))

  The left distributor.

Totality: total
Visibility: public export

distribl' : Bimonoidal cat add mul z i => cat (add (mul a b) (mul a c)) (mul a (add b c))

  The inverse of `distribl`, the left distributor.

Totality: total
Visibility: public export

distribr : Bimonoidal cat add mul z i => cat (mul (add a b) c) (add (mul a c) (mul b c))

  The right distributor.

Totality: total
Visibility: public export

distribr' : Bimonoidal cat add mul z i => cat (add (mul a c) (mul b c)) (mul (add a b) c)

  The inverse of `distribr`, the right distributor.

Totality: total
Visibility: public export

absorbl : Bimonoidal cat add mul z i => cat (mul a z) z

  The left absorbor.

Totality: total
Visibility: public export

absorbl' : Bimonoidal cat add mul z i => cat z (mul a z)

  The inverse of `absorbl`, the left absorbor.

Totality: total
Visibility: public export

absorbr : Bimonoidal cat add mul z i => cat (mul z a) z

  The right absorbor.

Totality: total
Visibility: public export

absorbr' : Bimonoidal cat add mul z i => cat z (mul z a)

  The inverse of `absorbr`, the right absorbor.

Totality: total
Visibility: public export

PreBimonoidal : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> Type

  A pre-bimonoidal category has a multiplicative structure that is
  premonoidal. See `PreMonoidal`.

Totality: total
Visibility: public export

RigCategory : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> 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).
  
  This is the interface-style definition of a rig category. For the
  record-style definition, see `Control.Category.Records.RigCategoryR`.

Totality: total
Visibility: public export

PreRigCategory : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> Type

  A pre-bimonoidal category has a multiplicative structure that is
  premonoidal. See `PreMonoidal`.

Totality: total
Visibility: public export

SymRigCategory : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> Type

  A symmetric rig category is a bimonoidal category where both the
  additive and multiplicative structures are symmetric.
  
  This is the interface-style definition of a symmetric rig category.
  For the record-style definition, see `Control.Category.Records.SymRigCategoryR`.

Totality: total
Visibility: public export

PreSymRigCategory : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> Type

  A pre-bimonoidal category has a multiplicative structure that is
  premonoidal. See `PreMonoidal`.

Totality: total
Visibility: public export

Distributive : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> Type

  A distributive category is a bimonoidal category whose
  multiplicative and additive structures are cartesian and
  cocartesian respectively.
  
  This is the interface-style definition of a distributuve category.
  For the record-style definition, see `Control.Category.Records.DistributiveR`.

Totality: total
Visibility: public export

PreDistributive : Hom obj -> (obj -> obj -> obj) -> (obj -> obj -> obj) -> obj -> obj -> Type

  A pre-bimonoidal category has a multiplicative structure that is
  premonoidal. See `PreMonoidal`.

Totality: total
Visibility: public export

Function : RigCategory (~~>) Either Pair Void ()

Totality: total
Visibility: public export

Function : SymRigCategory (~~>) Either Pair Void ()

Totality: total
Visibility: public export

Function : Distributive (~~>) Either Pair Void ()

Totality: total
Visibility: public export