0 | module Control.Category.Records.Cartesian
  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 Data.Morphisms
  8 |
  9 | %default total
 10 | %prefix_record_projections off
 11 |
 12 | ||| A monoidal category is *cartesian* if its tensor product coincides
 13 | ||| with the categorical product. This automatically implies that it
 14 | ||| is symmetric (see `Braided`).
 15 | |||
 16 | ||| See `Cartesian` for required laws.
 17 | public export
 18 | record CartesianR where
 19 |   constructor MkCartesianR
 20 |   hom : Hom obj
 21 |   tensor : obj -> obj -> obj
 22 |   unit : obj
 23 |   {auto impl : Cartesian hom tensor unit}
 24 |
 25 | ||| See `PreMonoidal`.
 26 | public export
 27 | PreCartesianR : Type
 28 | PreCartesianR = CartesianR
 29 |
 30 | namespace CartesianR
 31 |   ||| Convert this into a `CategoryR`.
 32 |   public export %inline
 33 |   (.categoryR) : (rec : CartesianR) -> CategoryR
 34 |   (.categoryR) (MkCartesianR {} {hom}) = MkCategoryR hom
 35 |
 36 |   ||| The identity morphism of an object `a`.
 37 |   public export %inline
 38 |   (.id) : (rec : CartesianR) -> {a : _} -> rec.hom a a
 39 |   (.id) (MkCartesianR {}) = id
 40 |
 41 |   ||| Binary right-to-left composition of morphisms.
 42 |   public export %inline
 43 |   (.comp) : (rec : CartesianR) -> {a,b,c : _} ->
 44 |             rec.hom b c -> rec.hom a b -> rec.hom a c
 45 |   (.comp) (MkCartesianR {}) = (.)
 46 |
 47 |
 48 |   ||| Return the tensor product as a `BifunctorR`.
 49 |   public export %inline
 50 |   (.tensorR) : (rec : CartesianR) -> EndoBifunctorR rec.categoryR
 51 |   (.tensorR) (MkCartesianR {} {tensor}) = MkBifunctorR tensor
 52 |
 53 |
 54 |   ||| Convert this into a `MonoidalR`.
 55 |   public export %inline
 56 |   (.monoidalR) : (rec : CartesianR) -> MonoidalR
 57 |   (.monoidalR) (MkCartesianR {} {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 : CartesianR) -> {a,b,c : _} ->
 62 |              rec.hom (rec.tensor (rec.tensor a b) c) (rec.tensor a (rec.tensor b c))
 63 |   (.assoc) (MkCartesianR {}) = assoc
 64 |
 65 |   ||| The right-biased associator. This must be the inverse of `(.assoc)`.
 66 |   public export %inline
 67 |   (.assoc') : (rec : CartesianR) -> {a,b,c : _} ->
 68 |               rec.hom (rec.tensor a (rec.tensor b c)) (rec.tensor (rec.tensor a b) c)
 69 |   (.assoc') (MkCartesianR {}) = assoc'
 70 |
 71 |   ||| The left unitor.
 72 |   public export %inline
 73 |   (.unitl) : (rec : CartesianR) -> {a : _} ->
 74 |              rec.hom (rec.tensor rec.unit a) a
 75 |   (.unitl) (MkCartesianR {}) = unitl
 76 |
 77 |   ||| The inverse of `(.unitl)`, the left unitor.
 78 |   public export %inline
 79 |   (.unitl') : (rec : CartesianR) -> {a : _} ->
 80 |               rec.hom a (rec.tensor rec.unit a)
 81 |   (.unitl') (MkCartesianR {}) = unitl'
 82 |
 83 |   ||| The right unitor.
 84 |   public export %inline
 85 |   (.unitr) : (rec : CartesianR) -> {a : _} ->
 86 |              rec.hom (rec.tensor a rec.unit) a
 87 |   (.unitr) (MkCartesianR {}) = unitr
 88 |
 89 |   ||| The inverse of `(.unitr)`, the right unitor.
 90 |   public export %inline
 91 |   (.unitr') : (rec : CartesianR) -> {a : _} ->
 92 |               rec.hom a (rec.tensor a rec.unit)
 93 |   (.unitr') (MkCartesianR {}) = unitr'
 94 |
 95 |
 96 |   ||| Convert this into a `BraidedR`.
 97 |   public export %inline
 98 |   (.braidedR) : (rec : CartesianR) -> BraidedR
 99 |   (.braidedR) (MkCartesianR {} {hom,tensor,unit}) =
100 |     MkBraidedR {hom,tensor,unit,impl = FromCartesian}
101 |
102 |   ||| Convert this into a `SymmetricR`.
103 |   public export %inline
104 |   (.symmetricR) : (rec : CartesianR) -> SymmetricR
105 |   (.symmetricR) (MkCartesianR {} {hom,tensor,unit}) =
106 |     MkSymmetricR {hom,tensor,unit,impl = FromCartesian}
107 |
108 |   ||| The braiding of the category.
109 |   public export %inline
110 |   (.braid) : (rec : CartesianR) -> {a,b : _} ->
111 |              rec.hom (rec.tensor a b) (rec.tensor b a)
112 |   (.braid) (MkCartesianR {}) = prod projr projl
113 |
114 |
115 |   ||| Convert this into a `CartesianR`.
116 |   public export %inline
117 |   (.cartesianR) : (rec : CartesianR) -> CartesianR
118 |   (.cartesianR) = id
119 |
120 |   ||| The left projection of the product.
121 |   public export %inline
122 |   (.projl) : (rec : CartesianR) -> {a,b : _} ->
123 |              rec.hom (rec.tensor a b) a
124 |   (.projl) (MkCartesianR {}) = projl
125 |
126 |   ||| The right projection of the product.
127 |   public export %inline
128 |   (.projr) : (rec : CartesianR) -> {a,b : _} ->
129 |              rec.hom (rec.tensor a b) b
130 |   (.projr) (MkCartesianR {}) = projr
131 |
132 |   ||| The universal property of the product.
133 |   public export %inline
134 |   (.prod) : (rec : CartesianR) -> {a,b,b' : _} ->
135 |             rec.hom a b -> rec.hom a b' -> rec.hom a (rec.tensor b b')
136 |   (.prod) (MkCartesianR {}) = prod
137 |
138 |   ||| The cojoin of the universal comonoid structure.
139 |   public export %inline
140 |   (.split) : (rec : CartesianR) -> {a : _} ->
141 |              rec.hom a (rec.tensor a a)
142 |   (.split) (MkCartesianR {}) = split
143 |
144 |   ||| The counit of the universal comonoid structure.
145 |   public export %inline
146 |   (.elim) : (rec : CartesianR) -> {a : _} ->
147 |             rec.hom a rec.unit
148 |   (.elim) (MkCartesianR {} {tensor}) = elim {ten=tensor}
149 |