0 | module Control.Category.Records.MonFunctor
  1 |
  2 | import Control.Category
  3 | import Control.Category.Records.Category
  4 | import Control.Category.Records.Monoidal
  5 | import Control.Category.Records.Functor
  6 |
  7 | %default total
  8 | %prefix_record_projections off
  9 |
 10 | ||| A lax monoidal functor from `cat` to `cat'`.
 11 | |||
 12 | ||| See `LaxMonFunctor` for required laws.
 13 | public export
 14 | record LaxMonFunctorR (cat,cat' : MonoidalR) where
 15 |   constructor MkLaxMonFunctorR
 16 |   fun : cat.obj -> cat'.obj
 17 |   {auto impl : LaxMonFunctor
 18 |     cat.hom cat.tensor cat.unit
 19 |     cat'.hom cat'.tensor cat'.unit fun}
 20 |
 21 | ||| A type synonym for a lax monoidal endofunctor.
 22 | public export %inline
 23 | LaxMonEndofunctorR : (cat : MonoidalR) -> Type
 24 | LaxMonEndofunctorR cat = LaxMonFunctorR cat cat
 25 |
 26 | namespace LaxMonFunctorR
 27 |   ||| Convert this into a `FunctorR`.
 28 |   public export %inline
 29 |   (.functorR) : (rec : LaxMonFunctorR cat cat') -> FunctorR cat.categoryR cat'.categoryR
 30 |   (.functorR) {cat=MkMonoidalR{},cat'=MkMonoidalR{}} (MkLaxMonFunctorR {} {fun}) = MkFunctorR fun
 31 |
 32 |   ||| Apply the functor to a morphism in `cat`.
 33 |   public export %inline
 34 |   (.map) : (rec : LaxMonFunctorR cat cat') -> {a,b : _} ->
 35 |            cat.hom a b -> cat'.hom (rec.fun a) (rec.fun b)
 36 |   (.map) {cat=MkMonoidalR{},cat'=MkMonoidalR{}} (MkLaxMonFunctorR {}) = map
 37 |
 38 |
 39 |   ||| Convert this into a `LaxMonFunctorR`.
 40 |   public export %inline
 41 |   (.laxMonFunctorR) : (rec : LaxMonFunctorR cat cat') -> LaxMonFunctorR cat cat'
 42 |   (.laxMonFunctorR) = id
 43 |
 44 |   ||| The lax monoidal functor action on the tensor product.
 45 |   public export %inline
 46 |   (.fjoin) : (rec : LaxMonFunctorR cat cat') -> {a,b : _} ->
 47 |              cat'.hom (cat'.tensor (rec.fun a) (rec.fun b)) (rec.fun (cat.tensor a b))
 48 |   (.fjoin) rec = fjoin @{rec.impl}
 49 |
 50 |   ||| The lax monoidal functor action on the unit object.
 51 |   public export %inline
 52 |   (.funit) : (rec : LaxMonFunctorR cat cat') -> cat'.hom cat'.unit (rec.fun cat.unit)
 53 |   (.funit) rec = funit @{rec.impl}
 54 |
 55 |
 56 | ||| A (strong) monoidal functor from `cat` to `cat'`.
 57 | |||
 58 | ||| See `MonFunctor` for required laws.
 59 | public export
 60 | record MonFunctorR (cat,cat' : MonoidalR) where
 61 |   constructor MkMonFunctorR
 62 |   fun : cat.obj -> cat'.obj
 63 |   {auto impl : MonFunctor
 64 |     cat.hom cat.tensor cat.unit
 65 |     cat'.hom cat'.tensor cat'.unit fun}
 66 |
 67 | ||| A type synonym for a monoidal endofunctor.
 68 | public export %inline
 69 | MonEndofunctorR : (cat : MonoidalR) -> Type
 70 | MonEndofunctorR cat = MonFunctorR cat cat
 71 |
 72 | namespace MonFunctorR
 73 |   ||| Convert this into a `FunctorR`.
 74 |   public export %inline
 75 |   (.functorR) : (rec : MonFunctorR cat cat') -> FunctorR cat.categoryR cat'.categoryR
 76 |   (.functorR) {cat=MkMonoidalR{},cat'=MkMonoidalR{}} (MkMonFunctorR {} {fun}) = MkFunctorR fun
 77 |
 78 |   ||| Apply the functor to a morphism in `cat`.
 79 |   public export %inline
 80 |   (.map) : (rec : MonFunctorR cat cat') -> {a,b : _} ->
 81 |            cat.hom a b -> cat'.hom (rec.fun a) (rec.fun b)
 82 |   (.map) {cat=MkMonoidalR{},cat'=MkMonoidalR{}} rec@(MkMonFunctorR {}) = map
 83 |
 84 |
 85 |   ||| Convert this into a `LaxMonFunctorR`.
 86 |   public export %inline
 87 |   (.laxMonFunctorR) : (rec : MonFunctorR cat cat') -> LaxMonFunctorR cat cat'
 88 |   (.laxMonFunctorR) {cat=MkMonoidalR{},cat'=MkMonoidalR{}} (MkMonFunctorR {} {fun}) = MkLaxMonFunctorR fun
 89 |
 90 |   ||| The monoidal functor action on the tensor product.
 91 |   public export %inline
 92 |   (.fjoin) : (rec : MonFunctorR cat cat') -> {a,b : _} ->
 93 |              cat'.hom (cat'.tensor (rec.fun a) (rec.fun b)) (rec.fun (cat.tensor a b))
 94 |   (.fjoin) {cat=MkMonoidalR {} {hom=cat,tensor=ten},cat'=MkMonoidalR {} {hom=cat',tensor=ten'}}
 95 |     rec@(MkMonFunctorR {}) = fjoin {cat,ten,cat',ten'}
 96 |
 97 |   ||| The monoidal functor action on the unit object.
 98 |   public export %inline
 99 |   (.funit) : (rec : MonFunctorR cat cat') -> cat'.hom cat'.unit (rec.fun cat.unit)
100 |   (.funit) {cat=MkMonoidalR {} {hom=cat,tensor=ten},cat'=MkMonoidalR {} {hom=cat',tensor=ten'}}
101 |     rec@(MkMonFunctorR {}) = funit {cat,ten,cat',ten'}
102 |
103 |
104 |   ||| Convert this into a `MonFunctorR`.
105 |   public export %inline
106 |   (.monFunctorR) : (rec : MonFunctorR cat cat') -> MonFunctorR cat cat'
107 |   (.monFunctorR) = id
108 |
109 |   ||| The inverse monoidal functor action on the tensor product.
110 |   public export %inline
111 |   (.fjoin') : (rec : MonFunctorR cat cat') -> {a,b : _} ->
112 |              cat'.hom (rec.fun (cat.tensor a b)) (cat'.tensor (rec.fun a) (rec.fun b))
113 |   (.fjoin') rec = fjoin' @{rec.impl}
114 |
115 |   ||| The inverse monoidal functor action on the unit object.
116 |   public export %inline
117 |   (.funit') : (rec : MonFunctorR cat cat') -> cat'.hom (rec.fun cat.unit) cat'.unit
118 |   (.funit') rec = funit' @{rec.impl}
119 |
120 |
121 | ||| An endofunctor has *tensorial strength* if it is compatible with a
122 | ||| monoidal category's tensor product.
123 | |||
124 | ||| See `StrongFunctor` for required laws.
125 | public export
126 | record StrongFunctorR (cat : MonoidalR) where
127 |   constructor MkStrongFunctorR
128 |   fun : cat.obj -> cat.obj
129 |   {auto impl : StrongFunctor cat.hom cat.tensor fun}
130 |
131 | namespace StrongFunctorR
132 |   ||| Convert this into a `FunctorR`.
133 |   public export %inline
134 |   (.functorR) : (rec : StrongFunctorR cat) -> EndofunctorR cat.categoryR
135 |   (.functorR) {cat=MkMonoidalR{}} (MkStrongFunctorR {} {fun}) = MkFunctorR fun
136 |
137 |   ||| Apply the functor to a morphism in `cat`.
138 |   public export %inline
139 |   (.map) : (rec : StrongFunctorR cat) -> {a,b : _} ->
140 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
141 |   (.map) {cat=MkMonoidalR{}} rec@(MkStrongFunctorR {}) = map
142 |
143 |   ||| The left tensor strength.
144 |   public export %inline
145 |   (.strongl) : (rec : StrongFunctorR cat) -> {a,b : _} ->
146 |                cat.hom (cat.tensor a (rec.fun b)) (rec.fun (cat.tensor a b))
147 |   (.strongl) rec = strongl @{rec.impl}
148 |
149 |   ||| The right tensor strength.
150 |   public export %inline
151 |   (.strongr) : (rec : StrongFunctorR cat) -> {a,b : _} ->
152 |                cat.hom (cat.tensor (rec.fun a) b) (rec.fun (cat.tensor a b))
153 |   (.strongr) rec = strongr @{rec.impl}
154 |
155 |
156 | ||| An endofunctor has *tensorial costrength* if it is compatible with
157 | ||| a monoidal category's tensor product in a way that is dual to a
158 | ||| tensorial strength.
159 | |||
160 | ||| See `CostrongFunctor` for required laws.
161 | public export
162 | record CostrongFunctorR (cat : MonoidalR) where
163 |   constructor MkCostrongFunctorR
164 |   fun : cat.obj -> cat.obj
165 |   {auto impl : CostrongFunctor cat.hom cat.tensor fun}
166 |
167 | namespace CostrongFunctorR
168 |   ||| Convert this into a `FunctorR`.
169 |   public export %inline
170 |   (.functorR) : (rec : CostrongFunctorR cat) -> EndofunctorR cat.categoryR
171 |   (.functorR) {cat=MkMonoidalR{}} (MkCostrongFunctorR {} {fun}) = MkFunctorR fun
172 |
173 |   ||| Apply the functor to a morphism in `cat`.
174 |   public export %inline
175 |   (.map) : (rec : CostrongFunctorR cat) -> {a,b : _} ->
176 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
177 |   (.map) {cat=MkMonoidalR{}} rec@(MkCostrongFunctorR {}) = map
178 |
179 |   ||| The left tensor costrength.
180 |   public export %inline
181 |   (.costrongl) : (rec : CostrongFunctorR cat) -> {a,b : _} ->
182 |                cat.hom (rec.fun (cat.tensor a b)) (cat.tensor a (rec.fun b))
183 |   (.costrongl) rec = costrongl @{rec.impl}
184 |
185 |   ||| The right tensor costrength.
186 |   public export %inline
187 |   (.costrongr) : (rec : CostrongFunctorR cat) -> {a,b : _} ->
188 |                cat.hom (rec.fun (cat.tensor a b)) (cat.tensor (rec.fun a) b)
189 |   (.costrongr) rec = costrongr @{rec.impl}
190 |