0 | module Control.Category.Records.Closed
  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 Control.Category.Records.Braided
  7 | import Control.Category.Records.Cartesian
  8 | import Data.Morphisms
  9 |
 10 | %default total
 11 | %prefix_record_projections off
 12 |
 13 | ||| A monoidal category is *closed* if it can meaningfully represent
 14 | ||| its morphisms as an object inside of itself. More specifically,
 15 | ||| the internal hom `ihom a b` is an object that encodes the set of
 16 | ||| morphisms from `a` to `b`.
 17 | |||
 18 | ||| Formally, a monoidal category is closed if the functor
 19 | ||| ``(`tensor` a)`` has a right adjoint functor `ihom a`.
 20 | |||
 21 | ||| See `Closed` for required laws.
 22 | public export
 23 | record ClosedR where
 24 |   constructor MkClosedR
 25 |   hom : Hom obj
 26 |   tensor, ihom : obj -> obj -> obj
 27 |   unit : obj
 28 |   {auto impl : Closed hom tensor ihom unit}
 29 |
 30 | namespace ClosedR
 31 |   ||| Convert this into a `CategoryR`.
 32 |   public export %inline
 33 |   (.categoryR) : (rec : ClosedR) -> CategoryR
 34 |   (.categoryR) (MkClosedR {} {hom}) = MkCategoryR hom
 35 |
 36 |   ||| The identity morphism of an object `a`.
 37 |   public export %inline
 38 |   (.id) : (rec : ClosedR) -> {a : _} -> rec.hom a a
 39 |   (.id) rec@(MkClosedR {}) = rec.categoryR.id
 40 |
 41 |   ||| Binary right-to-left composition of morphisms.
 42 |   public export %inline
 43 |   (.comp) : (rec : ClosedR) -> {a,b,c : _} ->
 44 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 45 |   (.comp) rec@(MkClosedR {}) = rec.categoryR.comp
 46 |
 47 |
 48 |   ||| Return the tensor product as a `BifunctorR`.
 49 |   public export %inline
 50 |   (.tensorR) : (rec : ClosedR) -> EndoBifunctorR rec.categoryR
 51 |   (.tensorR) (MkClosedR {} {tensor}) = MkBifunctorR tensor
 52 |
 53 |
 54 |   ||| Convert this into a `MonoidalR`.
 55 |   public export %inline
 56 |   (.monoidalR) : (rec : ClosedR) -> MonoidalR
 57 |   (.monoidalR) (MkClosedR {} {hom,tensor,unit}) = MkMonoidalR hom tensor unit
 58 |
 59 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
 60 |   public export %inline
 61 |   (.assoc) : (rec : ClosedR) -> {a,b,c : _} ->
 62 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
 63 |   (.assoc) rec@(MkClosedR {}) = rec.monoidalR.assoc
 64 |
 65 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
 66 |   public export %inline
 67 |   (.assoc') : (rec : ClosedR) -> {a,b,c : _} ->
 68 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
 69 |   (.assoc') rec@(MkClosedR {}) = rec.monoidalR.assoc'
 70 |
 71 |   ||| The left unitor.
 72 |   public export %inline
 73 |   (.unitl) : (rec : ClosedR) -> {a : _} ->
 74 |              rec.hom (rec.tensor rec.unit a) a
 75 |   (.unitl) rec@(MkClosedR {}) = rec.monoidalR.unitl
 76 |
 77 |   ||| The inverse of `(.unitl)`, the left unitor.
 78 |   public export %inline
 79 |   (.unitl') : (rec : ClosedR) -> {a : _} ->
 80 |               rec.hom a (rec.tensor rec.unit a)
 81 |   (.unitl') rec@(MkClosedR {}) = rec.monoidalR.unitl'
 82 |
 83 |   ||| The right unitor.
 84 |   public export %inline
 85 |   (.unitr) : (rec : ClosedR) -> {a : _} ->
 86 |              rec.hom (rec.tensor a rec.unit) a
 87 |   (.unitr) rec@(MkClosedR {}) = rec.monoidalR.unitr
 88 |
 89 |   ||| The inverse of `(.unitr)`, the right unitor.
 90 |   public export %inline
 91 |   (.unitr') : (rec : ClosedR) -> {a : _} ->
 92 |               rec.hom a (rec.tensor a rec.unit)
 93 |   (.unitr') rec@(MkClosedR {}) = rec.monoidalR.unitr'
 94 |
 95 |
 96 |   ||| Convert this into a `ClosedR`.
 97 |   public export %inline
 98 |   (.closedR) : (rec : ClosedR) -> ClosedR
 99 |   (.closedR) = id
100 |
101 |   ||| The currying transformation.
102 |   public export %inline
103 |   (.curry) : (rec : ClosedR) -> {a,b,c : _} ->
104 |              rec.hom (rec.tensor a b) c -> rec.hom a (rec.ihom b c)
105 |   (.curry) rec = curry @{rec.impl}
106 |
107 |   ||| The uncurrying transformation.
108 |   public export %inline
109 |   (.uncurry) : (rec : ClosedR) -> {a,b,c : _} ->
110 |                rec.hom a (rec.ihom b c) -> rec.hom (rec.tensor a b) c
111 |   (.uncurry) rec = uncurry @{rec.impl}
112 |
113 |   ||| The evaluation map.
114 |   public export %inline
115 |   (.eval) : (rec : ClosedR) -> {a,b : _} ->
116 |             rec.hom (rec.tensor (rec.ihom a b) a) b
117 |   (.eval) rec = eval @{rec.impl}
118 |
119 |   ||| The coevaluation map.
120 |   public export %inline
121 |   (.coeval) : (rec : ClosedR) -> {a,b : _} ->
122 |             rec.hom a (rec.ihom b (rec.tensor a b))
123 |   (.coeval) rec = coeval @{rec.impl}
124 |
125 |
126 | ||| A monoidal category that is both cartesian and closed.
127 | public export
128 | record CartesianClosedR where
129 |   constructor MkCartesianClosedR
130 |   hom : Hom obj
131 |   tensor, ihom : obj -> obj -> obj
132 |   unit : obj
133 |   {auto impl : CartesianClosed hom tensor ihom unit}
134 |
135 | ||| A shorter synonym for a cartesian closed category (`CartesianClosedR`).
136 | public export
137 | CCC : Type
138 | CCC = CartesianClosedR
139 |
140 | namespace CartesianClosedR
141 |   ||| Convert this into a `CategoryR`.
142 |   public export %inline
143 |   (.categoryR) : (rec : CartesianClosedR) -> CategoryR
144 |   (.categoryR) (MkCartesianClosedR {} {hom}) = MkCategoryR hom
145 |
146 |   ||| The identity morphism of an object `a`.
147 |   public export %inline
148 |   (.id) : (rec : CartesianClosedR) -> {a : _} -> rec.hom a a
149 |   (.id) rec@(MkCartesianClosedR {}) = rec.categoryR.id
150 |
151 |   ||| Binary right-to-left composition of morphisms.
152 |   public export %inline
153 |   (.comp) : (rec : CartesianClosedR) -> {a,b,c : _} ->
154 |             rec.hom b c -> rec.hom a b -> rec.hom a c
155 |   (.comp) rec@(MkCartesianClosedR {}) = rec.categoryR.comp
156 |
157 |
158 |   ||| Return the tensor product as a `BifunctorR`.
159 |   public export %inline
160 |   (.tensorR) : (rec : CartesianClosedR) -> EndoBifunctorR rec.categoryR
161 |   (.tensorR) (MkCartesianClosedR {} {tensor}) = MkBifunctorR tensor
162 |
163 |
164 |   ||| Convert this into a `MonoidalR`.
165 |   public export %inline
166 |   (.monoidalR) : (rec : CartesianClosedR) -> MonoidalR
167 |   (.monoidalR) (MkCartesianClosedR {} {hom,tensor,unit}) = MkMonoidalR hom tensor unit
168 |
169 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
170 |   public export %inline
171 |   (.assoc) : (rec : CartesianClosedR) -> {a,b,c : _} ->
172 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
173 |   (.assoc) rec@(MkCartesianClosedR {}) = rec.monoidalR.assoc
174 |
175 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
176 |   public export %inline
177 |   (.assoc') : (rec : CartesianClosedR) -> {a,b,c : _} ->
178 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
179 |   (.assoc') rec@(MkCartesianClosedR {}) = rec.monoidalR.assoc'
180 |
181 |   ||| The left unitor.
182 |   public export %inline
183 |   (.unitl) : (rec : CartesianClosedR) -> {a : _} ->
184 |              rec.hom (rec.tensor rec.unit a) a
185 |   (.unitl) rec@(MkCartesianClosedR {}) = rec.monoidalR.unitl
186 |
187 |   ||| The inverse of `(.unitl)`, the left unitor.
188 |   public export %inline
189 |   (.unitl') : (rec : CartesianClosedR) -> {a : _} ->
190 |               rec.hom a (rec.tensor rec.unit a)
191 |   (.unitl') rec@(MkCartesianClosedR {}) = rec.monoidalR.unitl'
192 |
193 |   ||| The right unitor.
194 |   public export %inline
195 |   (.unitr) : (rec : CartesianClosedR) -> {a : _} ->
196 |              rec.hom (rec.tensor a rec.unit) a
197 |   (.unitr) rec@(MkCartesianClosedR {}) = rec.monoidalR.unitr
198 |
199 |   ||| The inverse of `(.unitr)`, the right unitor.
200 |   public export %inline
201 |   (.unitr') : (rec : CartesianClosedR) -> {a : _} ->
202 |               rec.hom a (rec.tensor a rec.unit)
203 |   (.unitr') rec@(MkCartesianClosedR {}) = rec.monoidalR.unitr'
204 |
205 |
206 |   ||| Convert this into a `BraidedR`.
207 |   public export %inline
208 |   (.braidedR) : (rec : CartesianClosedR) -> BraidedR
209 |   (.braidedR) (MkCartesianClosedR {} {hom,tensor,unit}) =
210 |     MkBraidedR {hom,tensor,unit,impl = FromCartesian}
211 |
212 |   ||| The braiding of the category.
213 |   public export %inline
214 |   (.braid) : (rec : CartesianClosedR) -> {a,b : _} ->
215 |              rec.hom (rec.tensor a b) (rec.tensor b a)
216 |   (.braid) rec@(MkCartesianClosedR {}) = rec.braidedR.braid
217 |
218 |   ||| The inverse of `(.braid)`, the braiding of the category.
219 |   public export %inline
220 |   (.braid') : (rec : CartesianClosedR) -> {a,b : _} ->
221 |               rec.hom (rec.tensor b a) (rec.tensor a b)
222 |   (.braid') rec@(MkCartesianClosedR {}) = rec.braidedR.braid'
223 |
224 |
225 |   ||| Convert this into a `CartesianR`.
226 |   public export %inline
227 |   (.cartesianR) : (rec : CartesianClosedR) -> CartesianR
228 |   (.cartesianR) (MkCartesianClosedR {} {hom,tensor,unit}) = MkCartesianR {hom,tensor,unit}
229 |
230 |   ||| The left projection of the product.
231 |   public export %inline
232 |   (.projl) : (rec : CartesianClosedR) -> {a,b : _} ->
233 |              rec.hom (rec.tensor a b) a
234 |   (.projl) rec@(MkCartesianClosedR {}) = rec.cartesianR.projl
235 |
236 |   ||| The right projection of the product.
237 |   public export %inline
238 |   (.projr) : (rec : CartesianClosedR) -> {a,b : _} ->
239 |              rec.hom (rec.tensor a b) b
240 |   (.projr) rec@(MkCartesianClosedR {}) = rec.cartesianR.projr
241 |
242 |   ||| The universal property of the product.
243 |   public export %inline
244 |   (.prod) : (rec : CartesianClosedR) -> {a,b,b' : _} ->
245 |             rec.hom a b -> rec.hom a b' -> rec.hom a (rec.tensor b b')
246 |   (.prod) rec@(MkCartesianClosedR {}) = rec.cartesianR.prod
247 |
248 |   ||| The cojoin of the universal comonoid structure.
249 |   public export %inline
250 |   (.split) : (rec : CartesianClosedR) -> {a : _} ->
251 |              rec.hom a (rec.tensor a a)
252 |   (.split) rec@(MkCartesianClosedR {}) = rec.cartesianR.split
253 |
254 |   ||| The counit of the universal comonoid structure.
255 |   public export %inline
256 |   (.elim) : (rec : CartesianClosedR) -> {a : _} ->
257 |             rec.hom a rec.unit
258 |   (.elim) rec@(MkCartesianClosedR {}) = rec.cartesianR.elim
259 |
260 |
261 |   ||| Convert this into a `ClosedR`.
262 |   public export %inline
263 |   (.closedR) : (rec : CartesianClosedR) -> ClosedR
264 |   (.closedR) (MkCartesianClosedR {} {hom,tensor,ihom,unit}) =
265 |     MkClosedR {hom,tensor,ihom,unit}
266 |
267 |   ||| The currying transformation.
268 |   public export %inline
269 |   (.curry) : (rec : CartesianClosedR) -> {a,b,c : _} ->
270 |              rec.hom (rec.tensor a b) c -> rec.hom a (rec.ihom b c)
271 |   (.curry) rec@(MkCartesianClosedR {}) = rec.closedR.curry
272 |
273 |   ||| The uncurrying transformation.
274 |   public export %inline
275 |   (.uncurry) : (rec : CartesianClosedR) -> {a,b,c : _} ->
276 |                rec.hom a (rec.ihom b c) -> rec.hom (rec.tensor a b) c
277 |   (.uncurry) rec@(MkCartesianClosedR {}) = rec.closedR.uncurry
278 |
279 |   ||| The evaluation map.
280 |   public export %inline
281 |   (.eval) : (rec : CartesianClosedR) -> {a,b : _} ->
282 |             rec.hom (rec.tensor (rec.ihom a b) a) b
283 |   (.eval) rec@(MkCartesianClosedR {}) = rec.closedR.eval
284 |
285 |   ||| The coevaluation map.
286 |   public export %inline
287 |   (.coeval) : (rec : CartesianClosedR) -> {a,b : _} ->
288 |               rec.hom a (rec.ihom b (rec.tensor a b))
289 |   (.coeval) rec@(MkCartesianClosedR {}) = rec.closedR.coeval
290 |