Control.Category.Braided

Reexports

import public Data.Permutation

Definitions

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

  A monoidal category is *braided* when it is possible to flip the
  order of the tensor product in a coherent way, determined by the
  braiding isomorphism.
  
  This is the interface-style definition of a braided monoidal category.
  For the record-style definition, see `Control.Category.Records.BraidedR`.
  
  Laws:
  * `braid . braid' = braid' . braid = id`
  * `assoc . braid . assoc = mapr braid . assoc . mapl braid`
  * `assoc' . braid . assoc' = mapl braid . assoc' . mapr braid`

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

MkBraided

Methods:

braid : cat (ten a b) (ten b a)

  The braiding of the category.

braid' : cat (ten b a) (ten a b)

  The inverse of `braid`, the braiding of the category.
  
  The default definition sets this equal to `braid`, making the
  assumption that this braiding is symmetric. If it isn't, then
  both methods must be defined.

Implementations:

Braided Morphism Pair ()
Braided Morphism Either Void
Monad m => PreBraided (Kleislimorphism m) Pair ()
Monad m => Braided (Kleislimorphism m) Either Void

braid : Braided cat ten i => cat (ten a b) (ten b a)

  The braiding of the category.

Totality: total
Visibility: public export

braid' : Braided cat ten i => cat (ten b a) (ten a b)

  The inverse of `braid`, the braiding of the category.
  
  The default definition sets this equal to `braid`, making the
  assumption that this braiding is symmetric. If it isn't, then
  both methods must be defined.

Totality: total
Visibility: public export

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

  See `PreMonoidal`.

Totality: total
Visibility: public export

permuteDefault : Braided cat ten i => (p : Permutation (length xs)) -> cat (TenSeq ten i xs) (TenSeq ten i (permuteList xs p))

  The default implementation of `permute`. Note that this may be
  horribly inefficient on large tensor product sequences.

Totality: total
Visibility: public export

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

  A monoidal category is *symmetric* when it has a braiding that is
  equal to its own inverse.
  
  This is the interface-style definition of a symmetric monoidal category.
  For the record-style definition, see `Control.Category.Records.SymmetricR`.
  
  Laws:
  * `braid = braid'`
  * `permute identity = id`
  * `permute (compose p q) = permute p . permute q`

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

MkMonSymmetric

Methods:

permute : (p : Permutation (length xs)) -> cat (TenSeq ten i xs) (TenSeq ten i (permuteList xs p))

  Rearrange the values of a tensor product sequence by applying a
  permutation to its objects.
  
  This function exists purely for runtime efficiency. There is a
  default implementation of this function, `permuteDefault`.

Implementations:

MonSymmetric Morphism Pair ()
MonSymmetric Morphism Either Void
Monad m => PreSymmetric (Kleislimorphism m) Pair ()
Monad m => MonSymmetric (Kleislimorphism m) Either Void

permute : MonSymmetric cat ten i => (p : Permutation (length xs)) -> cat (TenSeq ten i xs) (TenSeq ten i (permuteList xs p))

  Rearrange the values of a tensor product sequence by applying a
  permutation to its objects.
  
  This function exists purely for runtime efficiency. There is a
  default implementation of this function, `permuteDefault`.

Totality: total
Visibility: public export

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

  See `PreMonoidal`.

Totality: total
Visibility: public export

swapAssoc : Braided cat ten i => cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i (ys ++ xs))

  Swap two halves of a tensor product sequence using the braiding.

Totality: total
Visibility: public export

swapAssoc' : Braided cat ten i => cat (TenSeq ten i (xs ++ ys)) (TenSeq ten i (ys ++ xs))

  Swap two halves of a tensor product sequence using the braiding.
  
  This uses `braid'` instead of `braid`. For symmetric monoidal
  categories, this is identical to `swapAssoc`.

Totality: total
Visibility: public export

bringToFront : Braided cat ten i => cat (TenSeq ten i (xs ++ (x :: ys))) (TenSeq ten i (x :: (xs ++ ys)))

  Bring a single object of a tensor product sequence to the front.

Totality: total
Visibility: public export

bringToFront' : Braided cat ten i => cat (TenSeq ten i (xs ++ (x :: ys))) (TenSeq ten i (x :: (xs ++ ys)))

  Bring a single object of a tensor product sequence to the front.
  
  This uses `braid'` instead of `braid`. For symmetric monoidal
  categories, this is identical to `bringToFront`.

Totality: total
Visibility: public export

insertFromFront : Braided cat ten i => cat (TenSeq ten i (x :: (xs ++ ys))) (TenSeq ten i (xs ++ (x :: ys)))

  Insert the first object of a tensor product sequence into a later
  position.
  
  This is the inverse of `bringToFront'`.

Totality: total
Visibility: public export

insertFromFront' : Braided cat ten i => cat (TenSeq ten i (x :: (xs ++ ys))) (TenSeq ten i (xs ++ (x :: ys)))

  Insert the first object of a tensor product sequence into a later
  position.
  
  This is the inverse of `bringToFront`. This uses `braid'` instead
  of `braid`. For symmetric monoidal categories, this is equivalent
  to `insertFromFront`.

Totality: total
Visibility: public export

sendToBack : Braided cat ten i => cat (TenSeq ten i (xs ++ (x :: ys))) (TenSeq ten i (xs ++ (ys ++ [x])))

  Send a single object of a tensor product sequence to the back.

Totality: total
Visibility: public export

sendToBack' : Braided cat ten i => cat (TenSeq ten i (xs ++ (x :: ys))) (TenSeq ten i (xs ++ (ys ++ [x])))

  Send a single object of a tensor product sequence to the back.
  
  This uses `braid'` instead of `braid`. For symmetric monoidal
  categories, this is identical to `sendToBack`.

Totality: total
Visibility: public export

insertFromBack : Braided cat ten i => cat (TenSeq ten i (xs ++ (ys ++ [x]))) (TenSeq ten i (xs ++ (x :: ys)))

  Insert the last object of a tensor product sequence into an earlier
  position.
  
  This is the inverse of `sendToBack'`.

Totality: total
Visibility: public export

insertFromBack' : Braided cat ten i => cat (TenSeq ten i (xs ++ (ys ++ [x]))) (TenSeq ten i (xs ++ (x :: ys)))

  Insert the last object of a tensor product sequence into an earlier
  position.
  
  This is the inverse of `sendToBack`. This uses `braid'` instead
  of `braid`. For symmetric monoidal categories, this is equivalent
  to `insertFromBack`.

Totality: total
Visibility: public export

BraidedMorPair : Braided Morphism Pair ()

Totality: total
Visibility: public export

BraidedMorEither : Braided Morphism Either Void

Totality: total
Visibility: public export

BraidedKleisliPair : Monad m => PreBraided (Kleislimorphism m) Pair ()

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

Totality: total
Visibility: public export

BraidedKleisliEither : Monad m => Braided (Kleislimorphism m) Either Void

Totality: total
Visibility: public export

FuncPair : Braided (~~>) Pair ()

Totality: total
Visibility: public export

FuncEither : Braided (~~>) Either Void

Totality: total
Visibility: public export

SymmetricMorEither : MonSymmetric Morphism Either Void

Totality: total
Visibility: public export

SymmetricKleisliPair : Monad m => PreSymmetric (Kleislimorphism m) Pair ()

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

Totality: total
Visibility: public export

SymmetricKleisliEither : Monad m => MonSymmetric (Kleislimorphism m) Either Void

Totality: total
Visibility: public export

FuncPair : MonSymmetric (~~>) Pair ()

Totality: total
Visibility: public export

FuncEither : MonSymmetric (~~>) Either Void

Totality: total
Visibility: public export