Control.Category.Monoidal

Definitions

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

  A *monoidal category* is a category equipped with a binary operator
  on its objects called the *tensor product* that respects its
  internal structure. This operation is required to be a monoid,
  that is to be associative and have an identity object (up to
  isomorphism).
  
  This is the interface-style definition of a monoidal category. For
  the record-style definition, see `Control.Category.Records.MonoidalR`.
  
  Laws:
  * `assoc . assoc' = assoc' . assoc = id`
  * `unitl . unitl' = unitl' . unitl = id`
  * `unitr . unitr' = unitr' . unitr = id`
  * `mapr unitl . assoc = mapl unitr` (triangle identity)
  * `assoc . assoc = mapr assoc . assoc . mapl assoc` (pentagon identity)

Parameters: cat, ten, i
Constraints: Category cat, CatEndoBifunctor cat ten
Constructor: 

MkMonoidal

Methods:

assoc : cat (ten (ten a b) c) (ten a (ten b c))

  The left-biased associator. This must be the inverse of `assoc'`.

assoc' : cat (ten a (ten b c)) (ten (ten a b) c)

  The right-biased associator. This must be the inverse of `assoc`.

unitl : cat (ten i a) a

  The left unitor.

unitl' : cat a (ten i a)

  The inverse of `unitl`, the left unitor.

unitr : cat (ten a i) a

  The right unitor.

unitr' : cat a (ten a i)

  The inverse of `unitr`, the right unitor.

Implementations:

Monoidal Morphism Pair ()

Monoidal Morphism Either Void

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

Monad m => Monoidal (Kleislimorphism m) Either Void

assoc : Monoidal cat ten i => cat (ten (ten a b) c) (ten a (ten b c))

  The left-biased associator. This must be the inverse of `assoc'`.

Totality: total
Visibility: public export

assoc' : Monoidal cat ten i => cat (ten a (ten b c)) (ten (ten a b) c)

  The right-biased associator. This must be the inverse of `assoc`.

Totality: total
Visibility: public export

unitl : Monoidal cat ten i => cat (ten i a) a

  The left unitor.

Totality: total
Visibility: public export

unitl' : Monoidal cat ten i => cat a (ten i a)

  The inverse of `unitl`, the left unitor.

Totality: total
Visibility: public export

unitr : Monoidal cat ten i => cat (ten a i) a

  The right unitor.

Totality: total
Visibility: public export

unitr' : Monoidal cat ten i => cat a (ten a i)

  The inverse of `unitr`, the right unitor.

Totality: total
Visibility: public export

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

  A type synonym that can be used to mark a category as merely being
  premonoidal, rather than a true monoidal category. These have the
  same laws, but allow the tensor product to be a binoidal functor.
  
  See https://github.com/tokinanpa/cats-and-arrows/tree/main/docs/CategoricalSins.md
  for more information on when/why this matters.

Totality: total
Visibility: public export

TenSeq : (obj -> obj -> obj) -> obj -> List obj -> obj

  A *tensor product sequence*, meaning a right-associated nested
  tensor product of objects. This structure is used by string
  diagram notation.

Totality: total
Visibility: public export

splitAssoc : Monoidal cat ten i => cat (TenSeq ten i (xs ++ ys)) (ten (TenSeq ten i xs) (TenSeq ten i ys))

  Split a tensor product sequence into two by reassociating.

Totality: total
Visibility: public export

mergeAssoc : Monoidal cat ten i => cat (ten (TenSeq ten i xs) (TenSeq ten i ys)) (TenSeq ten i (xs ++ ys))

  Merge two tensor product sequences into one by reassociating.

Totality: total
Visibility: public export

applyAssoc : Monoidal cat ten i => cat (TenSeq ten i ys) (TenSeq ten i ys') -> cat (TenSeq ten i (xs ++ (ys ++ zs))) (TenSeq ten i (xs ++ (ys' ++ zs)))

  Apply a morphism to the middle of a tensor product sequence.

Totality: total
Visibility: public export

FuncPair : Monoidal (~~>) Pair ()

Totality: total
Visibility: public export

FuncEither : Monoidal (~~>) Either Void

Totality: total
Visibility: public export

MonoidalMorPair : Monoidal Morphism Pair ()

Totality: total
Visibility: public export

MonoidalMorEither : Monoidal Morphism Either Void

Totality: total
Visibility: public export

MonoidalKleisliPair : Monad m => PreMonoidal (Kleislimorphism m) Pair ()

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

Totality: total
Visibility: public export

MonoidalKleisliEither : Monad m => Monoidal (Kleislimorphism m) Either Void

Totality: total
Visibility: public export

pairToHList : TenSeq Pair () ts -> HList ts

Totality: total
Visibility: public export

pairFromHList : HList ts -> TenSeq Pair () ts

Totality: total
Visibility: public export