Control.Category.Cartesian

Definitions

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

  A monoidal category is *cartesian* if its tensor product coincides
  with the categorical product. This automatically implies that it
  is symmetric (see `Braided`).
  
  This interface may be implemented in two equivalent ways: by giving
  a categorical product structure (`projl`, `projr`, `prod`) or a
  universal comonoid structure (`split`, `elim`). Each set of
  methods has a default definition in terms of the others.
  
  This is the interface-style definition of a cartesian monoidal category.
  For the record-style definition, see `Control.Category.Records.CartesianR`.
  
  Laws for `projl`, `projr`, `prod`:
  * `projl . prod f g = f`
  * `projr . prod f g = g`
  
  Laws for `split`, `elim`:
  * `unitl . mapl elim . split = id`
  * `unitr . mapr elim . split = id`

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

MkCartesian

Methods:

projl : cat (ten a b) a

  The left projection of the product.

projr : cat (ten a b) b

  The right projection of the product.

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

  The universal property of the product.

split : cat a (ten a a)

  The cojoin of the universal comonoid structure.

elim : cat a i

  The counit of the universal comonoid structure.

Implementations:

Cartesian Morphism Pair ()

Monad m => PreCartesian (Kleislimorphism m) Pair ()

projl : Cartesian cat ten i => cat (ten a b) a

  The left projection of the product.

Totality: total
Visibility: public export

projr : Cartesian cat ten i => cat (ten a b) b

  The right projection of the product.

Totality: total
Visibility: public export

prod : Cartesian cat ten i => cat a b -> cat a b' -> cat a (ten b b')

  The universal property of the product.

Totality: total
Visibility: public export

split : Cartesian cat ten i => cat a (ten a a)

  The cojoin of the universal comonoid structure.

Totality: total
Visibility: public export

elim : Cartesian cat ten i => cat a i

  The counit of the universal comonoid structure.

Totality: total
Visibility: public export

(&&&) : Cartesian cat ten i => cat a b -> cat a b' -> cat a (ten b b')

  An operator synonym for `prod`, the universal property of a
  cartesian monoidal category's product structure.

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

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

  See `PreMonoidal`.

Totality: total
Visibility: public export

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

  Project a single value out of a tensor product sequence by index.

Totality: total
Visibility: public export

Swizzle : Nat -> Type

  A compact representation of a function out of a tensor product
  sequence of size `n`. Used to rearrange/"swizzle" tensor products.

Totality: total
Visibility: public export

swizzleList : (xs : List a) -> Swizzle (length xs) -> List a

  Apply a `Swizzle` to a list, rearranging its elements.

Totality: total
Visibility: public export

swizzle : Cartesian cat ten i => (sw : Swizzle (length xs)) -> cat (TenSeq ten i xs) (TenSeq ten i (swizzleList xs sw))

  Apply a `Swizzle` to a tensor product sequence.

Totality: total
Visibility: public export

PreCartesianKleisli : Monad m => PreCartesian (Kleislimorphism m) Pair ()

  WARNING: This is a premonoidal category, not truly monoidal.

Totality: total
Visibility: public export