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