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) (MkBimonoidalR {}) = 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) (MkBimonoidalR {}) = (.)
 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) (MkBimonoidalR {}) = distribl
 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') (MkBimonoidalR {}) = distribl'
 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) (MkBimonoidalR {}) = distribr
 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') (MkBimonoidalR {}) = distribr'
 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) (MkBimonoidalR {} {impl}) = absorbl @{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') (MkBimonoidalR {} {impl}) = absorbl' @{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) (MkBimonoidalR {} {impl}) = absorbr @{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') (MkBimonoidalR {} {impl}) = absorbr' @{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) (MkRigCategoryR {}) = 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) (MkRigCategoryR {}) = (.)
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 `SymmetricR` with the additive tensor product.
164 |   public export %inline
165 |   (.addCatR) : (rec : RigCategoryR) -> SymmetricR
166 |   (.addCatR) (MkRigCategoryR {} {hom,add,zero}) = MkSymmetricR 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) (MkRigCategoryR {}) = 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') (MkRigCategoryR {}) = 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) (MkRigCategoryR {}) = 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') (MkRigCategoryR {}) = 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) (MkRigCategoryR {} {add,mul}) = absorbl {add,mul}
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') (MkRigCategoryR {} {add,mul}) = absorbl' {add,mul}
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) (MkRigCategoryR {} {add,mul}) = absorbr {add,mul}
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') (MkRigCategoryR {} {add,mul}) = absorbr' {add,mul}
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) (MkSymRigCategoryR {}) = 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) (MkSymRigCategoryR {}) = (.)
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 `SymmetricR` with the additive tensor product.
271 |   public export %inline
272 |   (.addCatR) : (rec : SymRigCategoryR) -> SymmetricR
273 |   (.addCatR) (MkSymRigCategoryR {} {hom,add,zero}) = MkSymmetricR hom add zero
274 |
275 |   ||| Convert this into a `SymmetricR` with the multiplicative tensor product.
276 |   public export %inline
277 |   (.mulCatR) : (rec : SymRigCategoryR) -> SymmetricR
278 |   (.mulCatR) (MkSymRigCategoryR {} {hom,mul,one}) = MkSymmetricR 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) (MkSymRigCategoryR {}) = 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') (MkSymRigCategoryR {}) = 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) (MkSymRigCategoryR {}) = 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') (MkSymRigCategoryR {}) = 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) (MkSymRigCategoryR {} {add,mul}) = absorbl {add,mul}
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') (MkSymRigCategoryR {} {add,mul}) = absorbl' {add,mul}
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) (MkSymRigCategoryR {} {add,mul}) = absorbr {add,mul}
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') (MkSymRigCategoryR {} {add,mul}) = absorbr' {add,mul}
329 |
330 |
331 |   ||| Convert this into a `RigCategoryR`.
332 |   public export %inline
333 |   (.rigCategoryR) : (rec : SymRigCategoryR) -> RigCategoryR
334 |   (.rigCategoryR) (MkSymRigCategoryR hom add mul z i) = MkRigCategoryR hom add mul z i
335 |
336 |   ||| Convert this into a `SymRigCategoryR`.
337 |   public export %inline
338 |   (.symRigCategoryR) : (rec : SymRigCategoryR) -> SymRigCategoryR
339 |   (.symRigCategoryR) = id
340 |
341 |
342 | public export
343 | record DistributiveR where
344 |   constructor MkDistributiveR
345 |   hom : Hom obj
346 |   add, mul : obj -> obj -> obj
347 |   zero, one : obj
348 |   {auto impl : Distributive hom add mul zero one}
349 |
350 | public export
351 | PreDistributiveR : Type
352 | PreDistributiveR = DistributiveR
353 |
354 | namespace DistributiveR
355 |   ||| Convert this into a `CategoryR`.
356 |   public export %inline
357 |   (.categoryR) : (rec : DistributiveR) -> CategoryR
358 |   (.categoryR) (MkDistributiveR {} {hom}) = MkCategoryR hom
359 |
360 |   ||| The identity morphism of an object `a`.
361 |   public export %inline
362 |   (.id) : (rec : DistributiveR) -> {a : _} -> rec.hom a a
363 |   (.id) (MkDistributiveR {}) = id
364 |
365 |   ||| Binary right-to-left composition of morphisms.
366 |   public export %inline
367 |   (.comp) : (rec : DistributiveR) -> {a,b,c : _} ->
368 |             rec.hom b c -> rec.hom a b -> rec.hom a c
369 |   (.comp) (MkDistributiveR {}) = (.)
370 |
371 |
372 |   ||| The additive tensor product as a `BifunctorR`.
373 |   public export %inline
374 |   (.addR) : (rec : DistributiveR) -> EndoBifunctorR rec.categoryR
375 |   (.addR) (MkDistributiveR {} {add}) = MkBifunctorR add
376 |
377 |   ||| The multiplicative tensor product as a `BifunctorR`.
378 |   public export %inline
379 |   (.mulR) : (rec : DistributiveR) -> EndoBifunctorR rec.categoryR
380 |   (.mulR) (MkDistributiveR {} {mul}) = MkBifunctorR mul
381 |
382 |   ||| Convert this into a `CocartesianR` with the additive tensor product.
383 |   public export %inline
384 |   (.addCatR) : (rec : DistributiveR) -> CocartesianR
385 |   (.addCatR) (MkDistributiveR {} {hom,add,zero}) = MkCocartesianR hom add zero
386 |
387 |   ||| Convert this into a `CartesianR` with the multiplicative tensor product.
388 |   public export %inline
389 |   (.mulCatR) : (rec : DistributiveR) -> CartesianR
390 |   (.mulCatR) (MkDistributiveR {} {hom,mul,one}) = MkCartesianR hom mul one
391 |
392 |
393 |   ||| Convert this into a `BimonoidalR`.
394 |   public export %inline
395 |   (.bimonoidalR) : (rec : DistributiveR) -> BimonoidalR
396 |   (.bimonoidalR) (MkDistributiveR hom add mul zero one) = MkBimonoidalR hom add mul zero one
397 |
398 |   ||| The left distributor.
399 |   public export %inline
400 |   (.distribl) : (rec : DistributiveR) -> {a,b,c : _} ->
401 |                 rec.hom (rec.mul a (rec.add b c)) (rec.add (rec.mul a b) (rec.mul a c))
402 |   (.distribl) (MkDistributiveR {}) = distribl
403 |
404 |   ||| The inverse of `(.distribl)`, the left distributor.
405 |   public export %inline
406 |   (.distribl') : (rec : DistributiveR) -> {a,b,c : _} ->
407 |                  rec.hom (rec.add (rec.mul a b) (rec.mul a c)) (rec.mul a (rec.add b c))
408 |   (.distribl') (MkDistributiveR {}) = distribl'
409 |
410 |   ||| The right distributor.
411 |   public export %inline
412 |   (.distribr) : (rec : DistributiveR) -> {a,b,c : _} ->
413 |                 rec.hom (rec.mul (rec.add a b) c) (rec.add (rec.mul a c) (rec.mul b c))
414 |   (.distribr) (MkDistributiveR {}) = distribr
415 |
416 |   ||| The inverse of `(.distribr)`, the right distributor.
417 |   public export %inline
418 |   (.distribr') : (rec : DistributiveR) -> {a,b,c : _} ->
419 |                  rec.hom (rec.add (rec.mul a c) (rec.mul b c)) (rec.mul (rec.add a b) c)
420 |   (.distribr') (MkDistributiveR {}) = distribr'
421 |
422 |   ||| The left absorbor.
423 |   public export %inline
424 |   (.absorbl) : (rec : DistributiveR) -> {a : _} -> rec.hom (rec.mul a rec.zero) rec.zero
425 |   (.absorbl) (MkDistributiveR {} {add,mul}) = absorbl {add,mul}
426 |
427 |   ||| The inverse of `(.absorbl)`, the left absorbor.
428 |   public export %inline
429 |   (.absorbl') : (rec : DistributiveR) -> {a : _} -> rec.hom rec.zero (rec.mul a rec.zero)
430 |   (.absorbl') (MkDistributiveR {} {add,mul}) = absorbl' {add,mul}
431 |
432 |   ||| The right absorbor.
433 |   public export %inline
434 |   (.absorbr) : (rec : DistributiveR) -> {a : _} -> rec.hom (rec.mul rec.zero a) rec.zero
435 |   (.absorbr) (MkDistributiveR {} {add,mul}) = absorbr {add,mul}
436 |
437 |   ||| The inverse of `(.absorbr)`, the right absorbor.
438 |   public export %inline
439 |   (.absorbr') : (rec : DistributiveR) -> {a : _} -> rec.hom rec.zero (rec.mul rec.zero a)
440 |   (.absorbr') (MkDistributiveR {} {add,mul}) = absorbr' {add,mul}
441 |
442 |
443 |   ||| Convert this into a `RigCategoryR`.
444 |   public export %inline
445 |   (.rigCategoryR) : (rec : DistributiveR) -> RigCategoryR
446 |   (.rigCategoryR) (MkDistributiveR hom add mul z i) = MkRigCategoryR hom add mul z i
447 |
448 |   ||| Convert this into a `SymRigCategoryR`.
449 |   public export %inline
450 |   (.symRigCategoryR) : (rec : DistributiveR) -> SymRigCategoryR
451 |   (.symRigCategoryR) (MkDistributiveR hom add mul z i) = MkSymRigCategoryR hom add mul z i
452 |
453 |   ||| Convert this into a `DistributiveR`.
454 |   public export %inline
455 |   (.distributiveR) : (rec : DistributiveR) -> DistributiveR
456 |   (.distributiveR) = id
457 |
458 |   ||| The left projection of the product.
459 |   public export %inline
460 |   (.projl) : (rec : DistributiveR) -> {a,b : _} ->
461 |              rec.hom (rec.mul a b) a
462 |   (.projl) (MkDistributiveR {}) = projl
463 |
464 |   ||| The right projection of the product.
465 |   public export %inline
466 |   (.projr) : (rec : DistributiveR) -> {a,b : _} ->
467 |              rec.hom (rec.mul a b) b
468 |   (.projr) (MkDistributiveR {}) = projr
469 |
470 |   ||| The universal property of the product.
471 |   public export %inline
472 |   (.prod) : (rec : DistributiveR) -> {a,b,b' : _} ->
473 |             rec.hom a b -> rec.hom a b' -> rec.hom a (rec.mul b b')
474 |   (.prod) (MkDistributiveR {}) = prod
475 |
476 |   ||| The cojoin of the universal comonoid structure.
477 |   public export %inline
478 |   (.split) : (rec : DistributiveR) -> {a : _} ->
479 |              rec.hom a (rec.mul a a)
480 |   (.split) (MkDistributiveR {}) = split
481 |
482 |   ||| The counit of the universal comonoid structure.
483 |   public export %inline
484 |   (.elim) : (rec : DistributiveR) -> {a : _} ->
485 |             rec.hom a rec.one
486 |   (.elim) (MkDistributiveR {} {mul}) = elim {ten=mul}
487 |
488 |   ||| The left injection of the coproduct.
489 |   public export %inline
490 |   (.injl) : (rec : DistributiveR) -> {a,b : _} ->
491 |             rec.hom a (rec.add a b)
492 |   (.injl) (MkDistributiveR {}) = injl
493 |
494 |   ||| The right injection of the coproduct.
495 |   public export %inline
496 |   (.injr) : (rec : DistributiveR) -> {a,b : _} ->
497 |             rec.hom b (rec.add a b)
498 |   (.injr) (MkDistributiveR {}) = injr
499 |
500 |   ||| The universal property of the coproduct.
501 |   public export %inline
502 |   (.coprod) : (rec : DistributiveR) -> {a,a',b : _} ->
503 |               rec.hom a b -> rec.hom a' b -> rec.hom (rec.add a a') b
504 |   (.coprod) (MkDistributiveR {}) = coprod
505 |
506 |   ||| The join of the universal monoid structure.
507 |   public export %inline
508 |   (.merge) : (rec : DistributiveR) -> {a : _} ->
509 |              rec.hom (rec.add a a) a
510 |   (.merge) (MkDistributiveR {}) = merge
511 |
512 |   ||| The unit of the universal monoid structure.
513 |   public export %inline
514 |   (.intro) : (rec : DistributiveR) -> {a : _} ->
515 |              rec.hom rec.zero a
516 |   (.intro) (MkDistributiveR {} {add}) = intro {ten=add}
517 |