0 | module Control.Category.Records.Monoidal
 1 |
 2 | import Control.Category
 3 | import Control.Category.Records.Category
 4 | import Control.Category.Records.Functor
 5 | import Data.Morphisms
 6 |
 7 | %default total
 8 | %prefix_record_projections off
 9 |
10 | ||| A *monoidal category* is a category equipped with a binary operator
11 | ||| on its objects called the *tensor product* that respects its
12 | ||| internal structure. This operation is required to be a monoid,
13 | ||| that is to be associative and have an identity object (up to
14 | ||| isomorphism).
15 | |||
16 | ||| See `Monoidal` for required laws.
17 | public export
18 | record MonoidalR where
19 |   constructor MkMonoidalR
20 |   hom : Hom obj
21 |   tensor : obj -> obj -> obj
22 |   unit : obj
23 |   {auto impl : Monoidal hom tensor unit}
24 |
25 | ||| See `PreMonoidal`.
26 | public export
27 | PreMonoidalR : Type
28 | PreMonoidalR = MonoidalR
29 |
30 | namespace MonoidalR
31 |   ||| Convert this into a `CategoryR`.
32 |   public export %inline
33 |   (.categoryR) : (rec : MonoidalR) -> CategoryR
34 |   (.categoryR) (MkMonoidalR {} {hom}) = MkCategoryR hom
35 |
36 |   ||| The identity morphism of an object `a`.
37 |   public export %inline
38 |   (.id) : (rec : MonoidalR) -> {a : _} -> rec.hom a a
39 |   (.id) rec@(MkMonoidalR {}) = rec.categoryR.id
40 |
41 |   ||| Binary right-to-left composition of morphisms.
42 |   public export %inline
43 |   (.comp) : (rec : MonoidalR) -> {a,b,c : _} ->
44 |             rec.hom b c -> rec.hom a b -> rec.hom a c
45 |   (.comp) rec@(MkMonoidalR {}) = rec.categoryR.comp
46 |
47 |
48 |   ||| Return the tensor product as a `BifunctorR`.
49 |   public export %inline
50 |   (.tensorR) : (rec : MonoidalR) -> EndoBifunctorR rec.categoryR
51 |   (.tensorR) (MkMonoidalR {} {tensor}) = MkBifunctorR tensor
52 |
53 |
54 |   ||| Convert this into a `MonoidalR`.
55 |   public export %inline
56 |   (.monoidalR) : (rec : MonoidalR) -> MonoidalR
57 |   (.monoidalR) = id
58 |
59 |   ||| The left-biased associator. This must be the inverse of `(.assoc')`.
60 |   public export %inline
61 |   (.assoc) : (rec : MonoidalR) -> {a,b,c : _} ->
62 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
63 |   (.assoc) rec = assoc @{rec.impl}
64 |
65 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
66 |   public export %inline
67 |   (.assoc') : (rec : MonoidalR) -> {a,b,c : _} ->
68 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
69 |   (.assoc') rec = assoc' @{rec.impl}
70 |
71 |   ||| The left unitor.
72 |   public export %inline
73 |   (.unitl) : (rec : MonoidalR) -> {a : _} ->
74 |              rec.hom (rec.tensor rec.unit a) a
75 |   (.unitl) rec = unitl @{rec.impl}
76 |
77 |   ||| The inverse of `(.unitl)`, the left unitor.
78 |   public export %inline
79 |   (.unitl') : (rec : MonoidalR) -> {a : _} ->
80 |               rec.hom a (rec.tensor rec.unit a)
81 |   (.unitl') rec = unitl' @{rec.impl}
82 |
83 |   ||| The right unitor.
84 |   public export %inline
85 |   (.unitr) : (rec : MonoidalR) -> {a : _} ->
86 |              rec.hom (rec.tensor a rec.unit) a
87 |   (.unitr) rec = unitr @{rec.impl}
88 |
89 |   ||| The inverse of `(.unitr)`, the right unitor.
90 |   public export %inline
91 |   (.unitr') : (rec : MonoidalR) -> {a : _} ->
92 |               rec.hom a (rec.tensor a rec.unit)
93 |   (.unitr') rec = unitr' @{rec.impl}
94 |