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.

Totality: total
Visibility: public export

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

  The right injection of the coproduct.

Totality: total
Visibility: public export

coprod : Cocartesian cat ten i => cat a b -> cat a' b -> cat (ten a a') b

  The universal property of the coproduct.

Totality: total
Visibility: public export

merge : Cocartesian cat ten i => cat (ten a a) a

  The join of the universal monoid structure.

Totality: total
Visibility: public export

intro : Cocartesian cat ten i => cat i a

  The unit of the universal monoid structure.

Totality: total
Visibility: public export

(\|/) : Cocartesian cat ten i => cat a b -> cat a' b -> cat (ten a a') b

  An operator synonym for `coprod`, the universal property of a
  cocartesian monoidal category's coproduct structure.

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

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

  See `PreMonoidal`.

Totality: total
Visibility: public export

inj : Cocartesian cat ten i => (x : Fin (length xs)) -> cat (index' xs x) (TenSeq ten i xs)

  Inject a single value into a coproduct sequence by index.

Totality: total
Visibility: public export

coswizzle : Cocartesian cat ten i => (sw : Swizzle (length xs)) -> cat (TenSeq ten i (swizzleList xs sw)) (TenSeq ten i xs)

  Apply a `Swizzle` to a coproduct sequence in reverse.
  
  This function is dual to `swizzle`.

Totality: total
Visibility: public export