0 | module Control.Category.Records.Bimonoidal
  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 Control.Category.Records.Cocartesian
  9 | import Data.Morphisms
 10 |
 11 | %default total
 12 | %prefix_record_projections off
 13 |
 14 | ||| A *bimonoidal category* is a category with two monoidal structures,
 15 | ||| one additive and one multiplicative, that are compatible with each
 16 | ||| other in a similar way to elementary algebra.
 17 | public export
 18 | record BimonoidalR where
 19 |   constructor MkBimonoidalR
 20 |   hom : Hom obj
 21 |   add, mul : obj -> obj -> obj
 22 |   zero, one : obj
 23 |   {auto impl : Bimonoidal hom add mul zero one}
 24 |
 25 | ||| See `PreMonoidal`.
 26 | public export
 27 | PreBimonoidalR : Type
 28 | PreBimonoidalR = BimonoidalR
 29 |
 30 | namespace BimonoidalR
 31 |   ||| Convert this into a `CategoryR`.
 32 |   public export %inline
 33 |   (.categoryR) : (rec : BimonoidalR) -> CategoryR
 34 |   (.categoryR) (MkBimonoidalR {} {hom}) = MkCategoryR hom
 35 |
 36 |   ||| The identity morphism of an object `a`.
 37 |   public export %inline
 38 |   (.id) : (rec : BimonoidalR) -> {a : _} -> rec.hom a a
 39 |   (.id) rec@(MkBimonoidalR {}) = rec.categoryR.id
 40 |
 41 |   ||| Binary right-to-left composition of morphisms.
 42 |   public export %inline
 43 |   (.comp) : (rec : BimonoidalR) -> {a,b,c : _} ->
 44 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 45 |   (.comp) rec@(MkBimonoidalR {}) = rec.categoryR.comp
 46 |
 47 |
 48 |   ||| The additive tensor product as a `BifunctorR`.
 49 |   public export %inline
 50 |   (.addR) : (rec : BimonoidalR) -> EndoBifunctorR rec.categoryR
 51 |   (.addR) (MkBimonoidalR {} {add}) = MkBifunctorR add
 52 |
 53 |   ||| The multiplicative tensor product as a `BifunctorR`.
 54 |   public export %inline
 55 |   (.mulR) : (rec : BimonoidalR) -> EndoBifunctorR rec.categoryR
 56 |   (.mulR) (MkBimonoidalR {} {mul}) = MkBifunctorR mul
 57 |
 58 |   ||| Convert this into a `MonoidalR` with the additive tensor product.
 59 |   public export %inline
 60 |   (.addCatR) : (rec : BimonoidalR) -> MonoidalR
 61 |   (.addCatR) (MkBimonoidalR {} {hom,add,zero}) = MkMonoidalR hom add zero
 62 |
 63 |   ||| Convert this into a `MonoidalR` with the multiplicative tensor product.
 64 |   public export %inline
 65 |   (.mulCatR) : (rec : BimonoidalR) -> MonoidalR
 66 |   (.mulCatR) (MkBimonoidalR {} {hom,mul,one}) = MkMonoidalR hom mul one
 67 |
 68 |
 69 |   ||| Convert this into a `BimonoidalR`.
 70 |   public export %inline
 71 |   (.bimonoidalR) : (rec : BimonoidalR) -> BimonoidalR
 72 |   (.bimonoidalR) = id
 73 |
 74 |   ||| The left distributor.
 75 |   public export %inline
 76 |   (.distribl) : (rec : BimonoidalR) -> {a,b,c : _} ->
 77 |                 rec.hom (rec.mul a (rec.add b c)) (rec.add (rec.mul a b) (rec.mul a c))
 78 |   (.distribl) rec = distribl @{rec.impl}
 79 |
 80 |   ||| The inverse of `(.distribl)`, the left distributor.
 81 |   public export %inline
 82 |   (.distribl') : (rec : BimonoidalR) -> {a,b,c : _} ->
 83 |                  rec.hom (rec.add (rec.mul a b) (rec.mul a c)) (rec.mul a (rec.add b c))
 84 |   (.distribl') rec = distribl' @{rec.impl}
 85 |
 86 |   ||| The right distributor.
 87 |   public export %inline
 88 |   (.distribr) : (rec : BimonoidalR) -> {a,b,c : _} ->
 89 |                 rec.hom (rec.mul (rec.add a b) c) (rec.add (rec.mul a c) (rec.mul b c))
 90 |   (.distribr) rec = distribr @{rec.impl}
 91 |
 92 |   ||| The inverse of `(.distribr)`, the right distributor.
 93 |   public export %inline
 94 |   (.distribr') : (rec : BimonoidalR) -> {a,b,c : _} ->
 95 |                  rec.hom (rec.add (rec.mul a c) (rec.mul b c)) (rec.mul (rec.add a b) c)
 96 |   (.distribr') rec = distribr' @{rec.impl}
 97 |
 98 |   ||| The left absorbor.
 99 |   public export %inline
100 |   (.absorbl) : (rec : BimonoidalR) -> {a : _} -> rec.hom (rec.mul a rec.zero) rec.zero
101 |   (.absorbl) rec = absorbl @{rec.impl}
102 |
103 |   ||| The inverse of `(.absorbl)`, the left absorbor.
104 |   public export %inline
105 |   (.absorbl') : (rec : BimonoidalR) -> {a : _} -> rec.hom rec.zero (rec.mul a rec.zero)
106 |   (.absorbl') rec = absorbl' @{rec.impl}
107 |
108 |   ||| The right absorbor.
109 |   public export %inline
110 |   (.absorbr) : (rec : BimonoidalR) -> {a : _} -> rec.hom (rec.mul rec.zero a) rec.zero
111 |   (.absorbr) rec = absorbr @{rec.impl}
112 |
113 |   ||| The inverse of `(.absorbr)`, the right absorbor.
114 |   public export %inline
115 |   (.absorbr') : (rec : BimonoidalR) -> {a : _} -> rec.hom rec.zero (rec.mul rec.zero a)
116 |   (.absorbr') rec = absorbr' @{rec.impl}
117 |
118 |
119 | ||| A rig category is a bimonoidal category whose additive structure
120 | ||| is symmetric. The name "rig" comes from the algebraic structure
121 | ||| the definition is based on (a ring without negatives).
122 | public export
123 | record RigCategoryR where
124 |   constructor MkRigCategoryR
125 |   hom : Hom obj
126 |   add, mul : obj -> obj -> obj
127 |   zero, one : obj
128 |   {auto impl : RigCategory hom add mul zero one}
129 |
130 | ||| See `PreMonoidal`.
131 | public export
132 | PreRigCategoryR : Type
133 | PreRigCategoryR = RigCategoryR
134 |
135 | namespace RigCategoryR
136 |   ||| Convert this into a `CategoryR`.
137 |   public export %inline
138 |   (.categoryR) : (rec : RigCategoryR) -> CategoryR
139 |   (.categoryR) (MkRigCategoryR {} {hom}) = MkCategoryR hom
140 |
141 |   ||| The identity morphism of an object `a`.
142 |   public export %inline
143 |   (.id) : (rec : RigCategoryR) -> {a : _} -> rec.hom a a
144 |   (.id) rec@(MkRigCategoryR {}) = rec.categoryR.id
145 |
146 |   ||| Binary right-to-left composition of morphisms.
147 |   public export %inline
148 |   (.comp) : (rec : RigCategoryR) -> {a,b,c : _} ->
149 |             rec.hom b c -> rec.hom a b -> rec.hom a c
150 |   (.comp) rec@(MkRigCategoryR {}) = rec.categoryR.comp
151 |
152 |
153 |   ||| The additive tensor product as a `BifunctorR`.
154 |   public export %inline
155 |   (.addR) : (rec : RigCategoryR) -> EndoBifunctorR rec.categoryR
156 |   (.addR) (MkRigCategoryR {} {add}) = MkBifunctorR add
157 |
158 |   ||| The multiplicative tensor product as a `BifunctorR`.
159 |   public export %inline
160 |   (.mulR) : (rec : RigCategoryR) -> EndoBifunctorR rec.categoryR
161 |   (.mulR) (MkRigCategoryR {} {mul}) = MkBifunctorR mul
162 |
163 |   ||| Convert this into a `BraidedR` with the additive tensor product.
164 |   public export %inline
165 |   (.addCatR) : (rec : RigCategoryR) -> BraidedR
166 |   (.addCatR) (MkRigCategoryR {} {hom,add,zero}) = MkBraidedR hom add zero
167 |
168 |   ||| Convert this into a `MonoidalR` with the multiplicative tensor product.
169 |   public export %inline
170 |   (.mulCatR) : (rec : RigCategoryR) -> MonoidalR
171 |   (.mulCatR) (MkRigCategoryR {} {hom,mul,one}) = MkMonoidalR hom mul one
172 |
173 |
174 |   ||| Convert this into a `BimonoidalR`.
175 |   public export %inline
176 |   (.bimonoidalR) : (rec : RigCategoryR) -> BimonoidalR
177 |   (.bimonoidalR) (MkRigCategoryR hom add mul zero one) = MkBimonoidalR hom add mul zero one
178 |
179 |   ||| The left distributor.
180 |   public export %inline
181 |   (.distribl) : (rec : RigCategoryR) -> {a,b,c : _} ->
182 |                 rec.hom (rec.mul a (rec.add b c)) (rec.add (rec.mul a b) (rec.mul a c))
183 |   (.distribl) rec@(MkRigCategoryR {}) = rec.bimonoidalR.distribl
184 |
185 |   ||| The inverse of `(.distribl)`, the left distributor.
186 |   public export %inline
187 |   (.distribl') : (rec : RigCategoryR) -> {a,b,c : _} ->
188 |                  rec.hom (rec.add (rec.mul a b) (rec.mul a c)) (rec.mul a (rec.add b c))
189 |   (.distribl') rec@(MkRigCategoryR {}) = rec.bimonoidalR.distribl'
190 |
191 |   ||| The right distributor.
192 |   public export %inline
193 |   (.distribr) : (rec : RigCategoryR) -> {a,b,c : _} ->
194 |                 rec.hom (rec.mul (rec.add a b) c) (rec.add (rec.mul a c) (rec.mul b c))
195 |   (.distribr) rec@(MkRigCategoryR {}) = rec.bimonoidalR.distribr
196 |
197 |   ||| The inverse of `(.distribr)`, the right distributor.
198 |   public export %inline
199 |   (.distribr') : (rec : RigCategoryR) -> {a,b,c : _} ->
200 |                  rec.hom (rec.add (rec.mul a c) (rec.mul b c)) (rec.mul (rec.add a b) c)
201 |   (.distribr') rec@(MkRigCategoryR {}) = rec.bimonoidalR.distribr'
202 |
203 |   ||| The left absorbor.
204 |   public export %inline
205 |   (.absorbl) : (rec : RigCategoryR) -> {a : _} -> rec.hom (rec.mul a rec.zero) rec.zero
206 |   (.absorbl) rec@(MkRigCategoryR {}) = rec.bimonoidalR.absorbl
207 |
208 |   ||| The inverse of `(.absorbl)`, the left absorbor.
209 |   public export %inline
210 |   (.absorbl') : (rec : RigCategoryR) -> {a : _} -> rec.hom rec.zero (rec.mul a rec.zero)
211 |   (.absorbl') rec@(MkRigCategoryR {}) = rec.bimonoidalR.absorbl'
212 |
213 |   ||| The right absorbor.
214 |   public export %inline
215 |   (.absorbr) : (rec : RigCategoryR) -> {a : _} -> rec.hom (rec.mul rec.zero a) rec.zero
216 |   (.absorbr) rec@(MkRigCategoryR {}) = rec.bimonoidalR.absorbr
217 |
218 |   ||| The inverse of `(.absorbr)`, the right absorbor.
219 |   public export %inline
220 |   (.absorbr') : (rec : RigCategoryR) -> {a : _} -> rec.hom rec.zero (rec.mul rec.zero a)
221 |   (.absorbr') rec@(MkRigCategoryR {}) = rec.bimonoidalR.absorbr'
222 |
223 |
224 |   ||| Convert this into a `RigCategoryR`.
225 |   public export %inline
226 |   (.rigCategoryR) : (rec : RigCategoryR) -> RigCategoryR
227 |   (.rigCategoryR) = id
228 |
229 |
230 | public export
231 | record SymRigCategoryR where
232 |   constructor MkSymRigCategoryR
233 |   hom : Hom obj
234 |   add, mul : obj -> obj -> obj
235 |   zero, one : obj
236 |   {auto impl : SymRigCategory hom add mul zero one}
237 |
238 | public export
239 | PreSymRigCategoryR : Type
240 | PreSymRigCategoryR = SymRigCategoryR
241 |
242 | namespace SymRigCategoryR
243 |   ||| Convert this into a `CategoryR`.
244 |   public export %inline
245 |   (.categoryR) : (rec : SymRigCategoryR) -> CategoryR
246 |   (.categoryR) (MkSymRigCategoryR {} {hom}) = MkCategoryR hom
247 |
248 |   ||| The identity morphism of an object `a`.
249 |   public export %inline
250 |   (.id) : (rec : SymRigCategoryR) -> {a : _} -> rec.hom a a
251 |   (.id) rec@(MkSymRigCategoryR {}) = rec.categoryR.id
252 |
253 |   ||| Binary right-to-left composition of morphisms.
254 |   public export %inline
255 |   (.comp) : (rec : SymRigCategoryR) -> {a,b,c : _} ->
256 |             rec.hom b c -> rec.hom a b -> rec.hom a c
257 |   (.comp) rec@(MkSymRigCategoryR {}) = rec.categoryR.comp
258 |
259 |
260 |   ||| The additive tensor product as a `BifunctorR`.
261 |   public export %inline
262 |   (.addR) : (rec : SymRigCategoryR) -> EndoBifunctorR rec.categoryR
263 |   (.addR) (MkSymRigCategoryR {} {add}) = MkBifunctorR add
264 |
265 |   ||| The multiplicative tensor product as a `BifunctorR`.
266 |   public export %inline
267 |   (.mulR) : (rec : SymRigCategoryR) -> EndoBifunctorR rec.categoryR
268 |   (.mulR) (MkSymRigCategoryR {} {mul}) = MkBifunctorR mul
269 |
270 |   ||| Convert this into a `BraidedR` with the additive tensor product.
271 |   public export %inline
272 |   (.addCatR) : (rec : SymRigCategoryR) -> BraidedR
273 |   (.addCatR) (MkSymRigCategoryR {} {hom,add,zero}) = MkBraidedR hom add zero
274 |
275 |   ||| Convert this into a `BraidedR` with the multiplicative tensor product.
276 |   public export %inline
277 |   (.mulCatR) : (rec : SymRigCategoryR) -> BraidedR
278 |   (.mulCatR) (MkSymRigCategoryR {} {hom,mul,one}) = MkBraidedR hom mul one
279 |
280 |
281 |   ||| Convert this into a `BimonoidalR`.
282 |   public export %inline
283 |   (.bimonoidalR) : (rec : SymRigCategoryR) -> BimonoidalR
284 |   (.bimonoidalR) (MkSymRigCategoryR hom add mul zero one) = MkBimonoidalR hom add mul zero one
285 |
286 |   ||| The left distributor.
287 |   public export %inline
288 |   (.distribl) : (rec : SymRigCategoryR) -> {a,b,c : _} ->
289 |                 rec.hom (rec.mul a (rec.add b c)) (rec.add (rec.mul a b) (rec.mul a c))
290 |   (.distribl) rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.distribl
291 |
292 |   ||| The inverse of `(.distribl)`, the left distributor.
293 |   public export %inline
294 |   (.distribl') : (rec : SymRigCategoryR) -> {a,b,c : _} ->
295 |                  rec.hom (rec.add (rec.mul a b) (rec.mul a c)) (rec.mul a (rec.add b c))
296 |   (.distribl') rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.distribl'
297 |
298 |   ||| The right distributor.
299 |   public export %inline
300 |   (.distribr) : (rec : SymRigCategoryR) -> {a,b,c : _} ->
301 |                 rec.hom (rec.mul (rec.add a b) c) (rec.add (rec.mul a c) (rec.mul b c))
302 |   (.distribr) rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.distribr
303 |
304 |   ||| The inverse of `(.distribr)`, the right distributor.
305 |   public export %inline
306 |   (.distribr') : (rec : SymRigCategoryR) -> {a,b,c : _} ->
307 |                  rec.hom (rec.add (rec.mul a c) (rec.mul b c)) (rec.mul (rec.add a b) c)
308 |   (.distribr') rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.distribr'
309 |
310 |   ||| The left absorbor.
311 |   public export %inline
312 |   (.absorbl) : (rec : SymRigCategoryR) -> {a : _} -> rec.hom (rec.mul a rec.zero) rec.zero
313 |   (.absorbl) rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.absorbl
314 |
315 |   ||| The inverse of `(.absorbl)`, the left absorbor.
316 |   public export %inline
317 |   (.absorbl') : (rec : SymRigCategoryR) -> {a : _} -> rec.hom rec.zero (rec.mul a rec.zero)
318 |   (.absorbl') rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.absorbl'
319 |
320 |   ||| The right absorbor.
321 |   public export %inline
322 |   (.absorbr) : (rec : SymRigCategoryR) -> {a : _} -> rec.hom (rec.mul rec.zero a) rec.zero
323 |   (.absorbr) rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.absorbr
324 |
325 |   ||| The inverse of `(.absorbr)`, the right absorbor.
326 |   public export %inline
327 |   (.absorbr') : (rec : SymRigCategoryR) -> {a : _} -> rec.hom rec.zero (rec.mul rec.zero a)
328 |   (.absorbr') rec@(MkSymRigCategoryR {}) = rec.bimonoidalR.absorbr'
329 |
330 |   ||| Convert this into a `RigCategoryR`.
331 |   public export %inline
332 |   (.rigCategoryR) : (rec : SymRigCategoryR) -> RigCategoryR
333 |   (.rigCategoryR) (MkSymRigCategoryR hom add mul z i) = MkRigCategoryR hom add mul z i
334 |
335 |   ||| Convert this into a `SymRigCategoryR`.
336 |   public export %inline
337 |   (.symRigCategoryR) : (rec : SymRigCategoryR) -> SymRigCategoryR
338 |   (.symRigCategoryR) = id
339 |
340 |
341 | public export
342 | record DistributiveR where
343 |   constructor MkDistributiveR
344 |   hom : Hom obj
345 |   add, mul : obj -> obj -> obj
346 |   zero, one : obj
347 |   {auto impl : Distributive hom add mul zero one}
348 |
349 | public export
350 | PreDistributiveR : Type
351 | PreDistributiveR = DistributiveR
352 |
353 | namespace DistributiveR
354 |   ||| Convert this into a `CategoryR`.
355 |   public export %inline
356 |   (.categoryR) : (rec : DistributiveR) -> CategoryR
357 |   (.categoryR) (MkDistributiveR {} {hom}) = MkCategoryR hom
358 |
359 |   ||| The identity morphism of an object `a`.
360 |   public export %inline
361 |   (.id) : (rec : DistributiveR) -> {a : _} -> rec.hom a a
362 |   (.id) rec@(MkDistributiveR {}) = rec.categoryR.id
363 |
364 |   ||| Binary right-to-left composition of morphisms.
365 |   public export %inline
366 |   (.comp) : (rec : DistributiveR) -> {a,b,c : _} ->
367 |             rec.hom b c -> rec.hom a b -> rec.hom a c
368 |   (.comp) rec@(MkDistributiveR {}) = rec.categoryR.comp
369 |
370 |
371 |   ||| The additive tensor product as a `BifunctorR`.
372 |   public export %inline
373 |   (.addR) : (rec : DistributiveR) -> EndoBifunctorR rec.categoryR
374 |   (.addR) (MkDistributiveR {} {add}) = MkBifunctorR add
375 |
376 |   ||| The multiplicative tensor product as a `BifunctorR`.
377 |   public export %inline
378 |   (.mulR) : (rec : DistributiveR) -> EndoBifunctorR rec.categoryR
379 |   (.mulR) (MkDistributiveR {} {mul}) = MkBifunctorR mul
380 |
381 |   ||| Convert this into a `CocartesianR` with the additive tensor product.
382 |   public export %inline
383 |   (.addCatR) : (rec : DistributiveR) -> CocartesianR
384 |   (.addCatR) (MkDistributiveR {} {hom,add,zero}) = MkCocartesianR hom add zero
385 |
386 |   ||| Convert this into a `CartesianR` with the multiplicative tensor product.
387 |   public export %inline
388 |   (.mulCatR) : (rec : DistributiveR) -> CartesianR
389 |   (.mulCatR) (MkDistributiveR {} {hom,mul,one}) = MkCartesianR hom mul one
390 |
391 |
392 |   ||| Convert this into a `BimonoidalR`.
393 |   public export %inline
394 |   (.bimonoidalR) : (rec : DistributiveR) -> BimonoidalR
395 |   (.bimonoidalR) (MkDistributiveR hom add mul zero one) = MkBimonoidalR hom add mul zero one
396 |
397 |   ||| The left distributor.
398 |   public export %inline
399 |   (.distribl) : (rec : DistributiveR) -> {a,b,c : _} ->
400 |                 rec.hom (rec.mul a (rec.add b c)) (rec.add (rec.mul a b) (rec.mul a c))
401 |   (.distribl) rec@(MkDistributiveR {}) = rec.bimonoidalR.distribl
402 |
403 |   ||| The inverse of `(.distribl)`, the left distributor.
404 |   public export %inline
405 |   (.distribl') : (rec : DistributiveR) -> {a,b,c : _} ->
406 |                  rec.hom (rec.add (rec.mul a b) (rec.mul a c)) (rec.mul a (rec.add b c))
407 |   (.distribl') rec@(MkDistributiveR {}) = rec.bimonoidalR.distribl'
408 |
409 |   ||| The right distributor.
410 |   public export %inline
411 |   (.distribr) : (rec : DistributiveR) -> {a,b,c : _} ->
412 |                 rec.hom (rec.mul (rec.add a b) c) (rec.add (rec.mul a c) (rec.mul b c))
413 |   (.distribr) rec@(MkDistributiveR {}) = rec.bimonoidalR.distribr
414 |
415 |   ||| The inverse of `(.distribr)`, the right distributor.
416 |   public export %inline
417 |   (.distribr') : (rec : DistributiveR) -> {a,b,c : _} ->
418 |                  rec.hom (rec.add (rec.mul a c) (rec.mul b c)) (rec.mul (rec.add a b) c)
419 |   (.distribr') rec@(MkDistributiveR {}) = rec.bimonoidalR.distribr'
420 |
421 |   ||| The left absorbor.
422 |   public export %inline
423 |   (.absorbl) : (rec : DistributiveR) -> {a : _} -> rec.hom (rec.mul a rec.zero) rec.zero
424 |   (.absorbl) rec@(MkDistributiveR {}) = rec.bimonoidalR.absorbl
425 |
426 |   ||| The inverse of `(.absorbl)`, the left absorbor.
427 |   public export %inline
428 |   (.absorbl') : (rec : DistributiveR) -> {a : _} -> rec.hom rec.zero (rec.mul a rec.zero)
429 |   (.absorbl') rec@(MkDistributiveR {}) = rec.bimonoidalR.absorbl'
430 |
431 |   ||| The right absorbor.
432 |   public export %inline
433 |   (.absorbr) : (rec : DistributiveR) -> {a : _} -> rec.hom (rec.mul rec.zero a) rec.zero
434 |   (.absorbr) rec@(MkDistributiveR {}) = rec.bimonoidalR.absorbr
435 |
436 |   ||| The inverse of `(.absorbr)`, the right absorbor.
437 |   public export %inline
438 |   (.absorbr') : (rec : DistributiveR) -> {a : _} -> rec.hom rec.zero (rec.mul rec.zero a)
439 |   (.absorbr') rec@(MkDistributiveR {}) = rec.bimonoidalR.absorbr'
440 |
441 |   ||| Convert this into a `RigCategoryR`.
442 |   public export %inline
443 |   (.rigCategoryR) : (rec : DistributiveR) -> RigCategoryR
444 |   (.rigCategoryR) (MkDistributiveR hom add mul z i) = MkRigCategoryR hom add mul z i
445 |
446 |   ||| Convert this into a `SymRigCategoryR`.
447 |   public export %inline
448 |   (.symRigCategoryR) : (rec : DistributiveR) -> SymRigCategoryR
449 |   (.symRigCategoryR) (MkDistributiveR hom add mul z i) = MkSymRigCategoryR hom add mul z i
450 |
451 |
452 |   ||| Convert this into a `DistributiveR`.
453 |   public export %inline
454 |   (.distributiveR) : (rec : DistributiveR) -> DistributiveR
455 |   (.distributiveR) = id
456 |
457 |   ||| The left projection of the product.
458 |   public export %inline
459 |   (.projl) : (rec : DistributiveR) -> {a,b : _} ->
460 |              rec.hom (rec.mul a b) a
461 |   (.projl) rec@(MkDistributiveR {}) = rec.mulCatR.projl
462 |
463 |   ||| The right projection of the product.
464 |   public export %inline
465 |   (.projr) : (rec : DistributiveR) -> {a,b : _} ->
466 |              rec.hom (rec.mul a b) b
467 |   (.projr) rec@(MkDistributiveR {}) = rec.mulCatR.projr
468 |
469 |   ||| The universal property of the product.
470 |   public export %inline
471 |   (.prod) : (rec : DistributiveR) -> {a,b,b' : _} ->
472 |             rec.hom a b -> rec.hom a b' -> rec.hom a (rec.mul b b')
473 |   (.prod) rec@(MkDistributiveR {}) = rec.mulCatR.prod
474 |
475 |   ||| The cojoin of the universal comonoid structure.
476 |   public export %inline
477 |   (.split) : (rec : DistributiveR) -> {a : _} ->
478 |              rec.hom a (rec.mul a a)
479 |   (.split) rec@(MkDistributiveR {}) = rec.mulCatR.split
480 |
481 |   ||| The counit of the universal comonoid structure.
482 |   public export %inline
483 |   (.elim) : (rec : DistributiveR) -> {a : _} ->
484 |             rec.hom a rec.one
485 |   (.elim) rec@(MkDistributiveR {}) = rec.mulCatR.elim
486 |
487 |   ||| The left injection of the coproduct.
488 |   public export %inline
489 |   (.injl) : (rec : DistributiveR) -> {a,b : _} ->
490 |             rec.hom a (rec.add a b)
491 |   (.injl) rec@(MkDistributiveR {}) = rec.addCatR.injl
492 |
493 |   ||| The right injection of the coproduct.
494 |   public export %inline
495 |   (.injr) : (rec : DistributiveR) -> {a,b : _} ->
496 |             rec.hom b (rec.add a b)
497 |   (.injr) rec@(MkDistributiveR {}) = rec.addCatR.injr
498 |
499 |   ||| The universal property of the coproduct.
500 |   public export %inline
501 |   (.coprod) : (rec : DistributiveR) -> {a,a',b : _} ->
502 |               rec.hom a b -> rec.hom a' b -> rec.hom (rec.add a a') b
503 |   (.coprod) rec@(MkDistributiveR {}) = rec.addCatR.coprod
504 |
505 |   ||| The join of the universal monoid structure.
506 |   public export %inline
507 |   (.merge) : (rec : DistributiveR) -> {a : _} ->
508 |              rec.hom (rec.add a a) a
509 |   (.merge) rec@(MkDistributiveR {}) = rec.addCatR.merge
510 |
511 |   ||| The unit of the universal monoid structure.
512 |   public export %inline
513 |   (.intro) : (rec : DistributiveR) -> {a : _} ->
514 |              rec.hom rec.zero a
515 |   (.intro) rec@(MkDistributiveR {}) = rec.addCatR.intro
516 |