Control.Category.Braided

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`
  
  Additionally, a braided monoidal category may be *symmetric*,
  requiring that `braid = braid'`. Since the only difference is in
  laws, the same interface is used for this case.

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

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 `bringToBack'`.

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 `bringToBack`. 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