0 | module Control.Category.Records.Braided
  1 |
  2 | import Control.Category
  3 | import Control.Category.Records.Category
  4 | import Control.Category.Records.Functor
  5 | import Control.Category.Records.Monoidal
  6 | import Data.Morphisms
  7 |
  8 | %default total
  9 | %prefix_record_projections off
 10 |
 11 | ||| A monoidal category is *braided* when it is possible to flip the
 12 | ||| order of the tensor product in a coherent way, determined by the
 13 | ||| braiding isomorphism.
 14 | |||
 15 | ||| Additionally, a braided monoidal category may be *symmetric*,
 16 | ||| requiring that `(.braid) = (.braid')`. Since the only difference
 17 | ||| is in laws, the same record is used for this case.
 18 | |||
 19 | ||| See `Braided` for required laws.
 20 | public export
 21 | record BraidedR where
 22 |   constructor MkBraidedR
 23 |   hom : Hom obj
 24 |   tensor : obj -> obj -> obj
 25 |   unit : obj
 26 |   {auto impl : Braided hom tensor unit}
 27 |
 28 | ||| See `PreMonoidal`.
 29 | public export
 30 | PreBraidedR : Type
 31 | PreBraidedR = BraidedR
 32 |
 33 | namespace BraidedR
 34 |   ||| Convert this into a `CategoryR`.
 35 |   public export %inline
 36 |   (.categoryR) : (rec : BraidedR) -> CategoryR
 37 |   (.categoryR) (MkBraidedR {} {hom}) = MkCategoryR hom
 38 |
 39 |   ||| The identity morphism of an object `a`.
 40 |   public export %inline
 41 |   (.id) : (rec : BraidedR) -> {a : _} -> rec.hom a a
 42 |   (.id) rec@(MkBraidedR {}) = rec.categoryR.id
 43 |
 44 |   ||| Binary right-to-left composition of morphisms.
 45 |   public export %inline
 46 |   (.comp) : (rec : BraidedR) -> {a,b,c : _} ->
 47 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 48 |   (.comp) rec@(MkBraidedR {}) = rec.categoryR.comp
 49 |
 50 |
 51 |   ||| Return the tensor product as a `BifunctorR`.
 52 |   public export %inline
 53 |   (.tensorR) : (rec : BraidedR) -> EndoBifunctorR rec.categoryR
 54 |   (.tensorR) (MkBraidedR {} {tensor}) = MkBifunctorR tensor
 55 |
 56 |
 57 |   ||| Convert this into a `MonoidalR`.
 58 |   public export %inline
 59 |   (.monoidalR) : (rec : BraidedR) -> MonoidalR
 60 |   (.monoidalR) (MkBraidedR {} {hom,tensor,unit}) = MkMonoidalR hom tensor unit
 61 |
 62 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
 63 |   public export %inline
 64 |   (.assoc) : (rec : BraidedR) -> {a,b,c : _} ->
 65 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
 66 |   (.assoc) rec@(MkBraidedR {}) = rec.monoidalR.assoc
 67 |
 68 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
 69 |   public export %inline
 70 |   (.assoc') : (rec : BraidedR) -> {a,b,c : _} ->
 71 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
 72 |   (.assoc') rec@(MkBraidedR {}) = rec.monoidalR.assoc'
 73 |
 74 |   ||| The left unitor.
 75 |   public export %inline
 76 |   (.unitl) : (rec : BraidedR) -> {a : _} ->
 77 |              rec.hom (rec.tensor rec.unit a) a
 78 |   (.unitl) rec@(MkBraidedR {}) = rec.monoidalR.unitl
 79 |
 80 |   ||| The inverse of `(.unitl)`, the left unitor.
 81 |   public export %inline
 82 |   (.unitl') : (rec : BraidedR) -> {a : _} ->
 83 |               rec.hom a (rec.tensor rec.unit a)
 84 |   (.unitl') rec@(MkBraidedR {}) = rec.monoidalR.unitl'
 85 |
 86 |   ||| The right unitor.
 87 |   public export %inline
 88 |   (.unitr) : (rec : BraidedR) -> {a : _} ->
 89 |              rec.hom (rec.tensor a rec.unit) a
 90 |   (.unitr) rec@(MkBraidedR {}) = rec.monoidalR.unitr
 91 |
 92 |   ||| The inverse of `(.unitr)`, the right unitor.
 93 |   public export %inline
 94 |   (.unitr') : (rec : BraidedR) -> {a : _} ->
 95 |               rec.hom a (rec.tensor a rec.unit)
 96 |   (.unitr') rec@(MkBraidedR {}) = rec.monoidalR.unitr'
 97 |
 98 |
 99 |   ||| Convert this into a `BraidedR`.
100 |   public export %inline
101 |   (.braidedR) : (rec : BraidedR) -> BraidedR
102 |   (.braidedR) = id
103 |
104 |   ||| The braiding of the category.
105 |   public export %inline
106 |   (.braid) : (rec : BraidedR) -> {a,b : _} ->
107 |              rec.hom (rec.tensor a b) (rec.tensor b a)
108 |   (.braid) rec = braid @{rec.impl}
109 |
110 |   ||| The inverse of `(.braid)`, the braiding of the category.
111 |   public export %inline
112 |   (.braid') : (rec : BraidedR) -> {a,b : _} ->
113 |               rec.hom (rec.tensor b a) (rec.tensor a b)
114 |   (.braid') rec = braid' @{rec.impl}
115 |
116 |   ||| Invert the braiding of the monoidal category. If the braiding is
117 |   ||| symmetric, this does nothing.
118 |   public export
119 |   (.flipBraid) : (rec : BraidedR) -> BraidedR
120 |   (.flipBraid) (MkBraidedR hom ten i) =
121 |     MkBraidedR hom ten i {impl = FlipBraid}
122 |