
   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) (MkClosedR {}) = 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) (MkClosedR {}) = (.)
  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) (MkClosedR {}) = 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') (MkClosedR {}) = 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) (MkClosedR {}) = 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') (MkClosedR {}) = 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) (MkClosedR {}) = 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') (MkClosedR {}) = 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) (MkClosedR {}) = curry
 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) (MkClosedR {}) = uncurry
 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) (MkClosedR {}) = eval
 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) (MkClosedR {} {tensor}) = coeval {ten=tensor}
 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = (.)
 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) (MkCartesianClosedR {}) = 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') (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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') (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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') (MkCartesianClosedR {}) = 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 |   ||| Convert this into a `SymmetricR`.
 213 |   public export %inline
 214 |   (.symmetricR) : (rec : CartesianClosedR) -> SymmetricR
 215 |   (.symmetricR) (MkCartesianClosedR {} {hom,tensor,unit}) =
 216 |     MkSymmetricR {hom,tensor,unit,impl = FromCartesian}
 217 | 
 218 |   ||| The braiding of the category.
 219 |   public export %inline
 220 |   (.braid) : (rec : CartesianClosedR) -> {a,b : _} ->
 221 |              rec.hom (rec.tensor a b) (rec.tensor b a)
 222 |   (.braid) (MkCartesianClosedR {}) = prod projr projl
 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {} {tensor}) = elim {ten=tensor}
 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {}) = 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) (MkCartesianClosedR {} {tensor}) = coeval {ten=tensor}
 290 |