Control.Category.Cocartesian

Definitions

interface Cocartesian : Hom obj -> (obj -> obj -> obj) -> obj -> Type

  A monoidal category is *cocartesian* if its tensor product
  coincides with the categorical coproduct. This automatically
  implies that it is symmetric (see `Braided`).
  
  This interface may be implemented in two equivalent ways: by giving
  a categorical coproduct structure (`injl`, `injr`, `coprod`) or a
  universal monoid structure (`merge`, `intro`). Each set of methods
  has a default definition in terms of the others.
  
  This is the interface-style definition of a cocartesian monoidal category.
  For the record-style definition, see `Control.Category.Records.CocartesianR`.
  
  Laws for `injl`, `injr`, `coprod`:
  * `coprod f g . injl = f`
  * `coprod f g . injr = g`
  
  Laws for `merge`, `intro`:
  * `merge . mapl intro . unitl' = id`
  * `merge . mapr intro . unitr' = id`

Parameters: cat, ten, i
Constraints: Monoidal cat ten i
Constructor:

MkCocartesian

Methods:

injl : cat a (ten a b)

  The left injection of the coproduct.

injr : cat b (ten a b)

  The right injection of the coproduct.

coprod : cat a b -> cat a' b -> cat (ten a a') b

  The universal property of the coproduct.

merge : cat (ten a a) a

  The join of the universal monoid structure.

intro : cat i a

  The unit of the universal monoid structure.

Implementations:

Cocartesian Morphism Either Void
Monad m => Cocartesian (Kleislimorphism m) Either Void

injl : Cocartesian cat ten i => cat a (ten a b)

  The left injection of the coproduct.