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 | ||| See `Braided` for required laws.
 16 | public export
 17 | record BraidedR where
 18 |   constructor MkBraidedR
 19 |   hom : Hom obj
 20 |   tensor : obj -> obj -> obj
 21 |   unit : obj
 22 |   {auto impl : Braided hom tensor unit}
 23 |
 24 | ||| See `PreMonoidal`.
 25 | public export
 26 | PreBraidedR : Type
 27 | PreBraidedR = BraidedR
 28 |
 29 | namespace BraidedR
 30 |   ||| Convert this into a `CategoryR`.
 31 |   public export %inline
 32 |   (.categoryR) : (rec : BraidedR) -> CategoryR
 33 |   (.categoryR) (MkBraidedR {} {hom}) = MkCategoryR hom
 34 |
 35 |   ||| The identity morphism of an object `a`.
 36 |   public export %inline
 37 |   (.id) : (rec : BraidedR) -> {a : _} -> rec.hom a a
 38 |   (.id) (MkBraidedR {}) = id
 39 |
 40 |   ||| Binary right-to-left composition of morphisms.
 41 |   public export %inline
 42 |   (.comp) : (rec : BraidedR) -> {a,b,c : _} ->
 43 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 44 |   (.comp) (MkBraidedR {}) = (.)
 45 |
 46 |
 47 |   ||| Return the tensor product as a `BifunctorR`.
 48 |   public export %inline
 49 |   (.tensorR) : (rec : BraidedR) -> EndoBifunctorR rec.categoryR
 50 |   (.tensorR) (MkBraidedR {} {tensor}) = MkBifunctorR tensor
 51 |
 52 |
 53 |   ||| Convert this into a `MonoidalR`.
 54 |   public export %inline
 55 |   (.monoidalR) : (rec : BraidedR) -> MonoidalR
 56 |   (.monoidalR) (MkBraidedR {} {hom,tensor,unit}) = MkMonoidalR hom tensor unit
 57 |
 58 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
 59 |   public export %inline
 60 |   (.assoc) : (rec : BraidedR) -> {a,b,c : _} ->
 61 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
 62 |   (.assoc) (MkBraidedR {}) = assoc
 63 |
 64 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
 65 |   public export %inline
 66 |   (.assoc') : (rec : BraidedR) -> {a,b,c : _} ->
 67 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
 68 |   (.assoc') (MkBraidedR {}) = assoc'
 69 |
 70 |   ||| The left unitor.
 71 |   public export %inline
 72 |   (.unitl) : (rec : BraidedR) -> {a : _} ->
 73 |              rec.hom (rec.tensor rec.unit a) a
 74 |   (.unitl) (MkBraidedR {}) = unitl
 75 |
 76 |   ||| The inverse of `(.unitl)`, the left unitor.
 77 |   public export %inline
 78 |   (.unitl') : (rec : BraidedR) -> {a : _} ->
 79 |               rec.hom a (rec.tensor rec.unit a)
 80 |   (.unitl') (MkBraidedR {}) = unitl'
 81 |
 82 |   ||| The right unitor.
 83 |   public export %inline
 84 |   (.unitr) : (rec : BraidedR) -> {a : _} ->
 85 |              rec.hom (rec.tensor a rec.unit) a
 86 |   (.unitr) (MkBraidedR {}) = unitr
 87 |
 88 |   ||| The inverse of `(.unitr)`, the right unitor.
 89 |   public export %inline
 90 |   (.unitr') : (rec : BraidedR) -> {a : _} ->
 91 |               rec.hom a (rec.tensor a rec.unit)
 92 |   (.unitr') (MkBraidedR {}) = unitr'
 93 |
 94 |
 95 |   ||| Convert this into a `BraidedR`.
 96 |   public export %inline
 97 |   (.braidedR) : (rec : BraidedR) -> BraidedR
 98 |   (.braidedR) = id
 99 |
100 |   ||| The braiding of the category.
101 |   public export %inline
102 |   (.braid) : (rec : BraidedR) -> {a,b : _} ->
103 |              rec.hom (rec.tensor a b) (rec.tensor b a)
104 |   (.braid) (MkBraidedR {}) = braid
105 |
106 |   ||| The inverse of `(.braid)`, the braiding of the category.
107 |   public export %inline
108 |   (.braid') : (rec : BraidedR) -> {a,b : _} ->
109 |               rec.hom (rec.tensor b a) (rec.tensor a b)
110 |   (.braid') (MkBraidedR {}) = braid'
111 |
112 |   ||| Invert the braiding of the monoidal category. If the braiding is
113 |   ||| symmetric, this does nothing.
114 |   public export
115 |   (.flipBraid) : (rec : BraidedR) -> BraidedR
116 |   (.flipBraid) (MkBraidedR hom ten i) =
117 |     MkBraidedR hom ten i {impl = FlipBraid}
118 |
119 |
120 | ||| A monoidal category is *symmetric* when it has a braiding that is
121 | ||| equal to its own inverse.
122 | |||
123 | ||| See `MonSymmetric` for required laws.
124 | public export
125 | record SymmetricR where
126 |   constructor MkSymmetricR
127 |   hom : Hom obj
128 |   tensor : obj -> obj -> obj
129 |   unit : obj
130 |   {auto impl : MonSymmetric hom tensor unit}
131 |
132 | ||| See `PreMonoidal`.
133 | public export
134 | PreSymmetricR : Type
135 | PreSymmetricR = SymmetricR
136 |
137 | namespace SymmetricR
138 |   ||| Convert this into a `CategoryR`.
139 |   public export %inline
140 |   (.categoryR) : (rec : SymmetricR) -> CategoryR
141 |   (.categoryR) (MkSymmetricR {} {hom}) = MkCategoryR hom
142 |
143 |   ||| The identity morphism of an object `a`.
144 |   public export %inline
145 |   (.id) : (rec : SymmetricR) -> {a : _} -> rec.hom a a
146 |   (.id) (MkSymmetricR {}) = id
147 |
148 |   ||| Binary right-to-left composition of morphisms.
149 |   public export %inline
150 |   (.comp) : (rec : SymmetricR) -> {a,b,c : _} ->
151 |             rec.hom b c -> rec.hom a b -> rec.hom a c
152 |   (.comp) (MkSymmetricR {}) = (.)
153 |
154 |
155 |   ||| Return the tensor product as a `BifunctorR`.
156 |   public export %inline
157 |   (.tensorR) : (rec : SymmetricR) -> EndoBifunctorR rec.categoryR
158 |   (.tensorR) (MkSymmetricR {} {tensor}) = MkBifunctorR tensor
159 |
160 |
161 |   ||| Convert this into a `MonoidalR`.
162 |   public export %inline
163 |   (.monoidalR) : (rec : SymmetricR) -> MonoidalR
164 |   (.monoidalR) (MkSymmetricR {} {hom,tensor,unit}) = MkMonoidalR hom tensor unit
165 |
166 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
167 |   public export %inline
168 |   (.assoc) : (rec : SymmetricR) -> {a,b,c : _} ->
169 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
170 |   (.assoc) (MkSymmetricR {}) = assoc
171 |
172 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
173 |   public export %inline
174 |   (.assoc') : (rec : SymmetricR) -> {a,b,c : _} ->
175 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
176 |   (.assoc') (MkSymmetricR {}) = assoc'
177 |
178 |   ||| The left unitor.
179 |   public export %inline
180 |   (.unitl) : (rec : SymmetricR) -> {a : _} ->
181 |              rec.hom (rec.tensor rec.unit a) a
182 |   (.unitl) (MkSymmetricR {}) = unitl
183 |
184 |   ||| The inverse of `(.unitl)`, the left unitor.
185 |   public export %inline
186 |   (.unitl') : (rec : SymmetricR) -> {a : _} ->
187 |               rec.hom a (rec.tensor rec.unit a)
188 |   (.unitl') (MkSymmetricR {}) = unitl'
189 |
190 |   ||| The right unitor.
191 |   public export %inline
192 |   (.unitr) : (rec : SymmetricR) -> {a : _} ->
193 |              rec.hom (rec.tensor a rec.unit) a
194 |   (.unitr) (MkSymmetricR {}) = unitr
195 |
196 |   ||| The inverse of `(.unitr)`, the right unitor.
197 |   public export %inline
198 |   (.unitr') : (rec : SymmetricR) -> {a : _} ->
199 |               rec.hom a (rec.tensor a rec.unit)
200 |   (.unitr') (MkSymmetricR {}) = unitr'
201 |
202 |
203 |   ||| Convert this into a `BraidedR`.
204 |   public export %inline
205 |   (.braidedR) : (rec : SymmetricR) -> BraidedR
206 |   (.braidedR) (MkSymmetricR {} {hom,tensor,unit}) = MkBraidedR hom tensor unit
207 |
208 |   ||| The braiding of the category.
209 |   public export %inline
210 |   (.braid) : (rec : SymmetricR) -> {a,b : _} ->
211 |              rec.hom (rec.tensor a b) (rec.tensor b a)
212 |   (.braid) (MkSymmetricR {}) = braid
213 |