0 | module Control.Category.MonFunctor
2 | import Control.Category.Core
3 | import Control.Category.Functor
4 | import Control.Category.Monoidal
5 | import Data.Morphisms
23 | interface CatFunctor cat cat' f => LaxMonFunctor
24 | (0 cat : Hom obj) (0 ten : obj -> obj -> obj) (0 i : obj)
25 | (0 cat' : Hom obj') (0 ten' : obj' -> obj' -> obj') (0 i' : obj')
26 | (0 f : obj -> obj') | cat,ten,cat',ten',f where
27 | constructor MkLaxMonFunctor
29 | fjoin : {a,b : _} -> cat' (f a `ten'` f b) (f (a `ten` b))
31 | funit : cat' i' (f i)
39 | public export %inline
40 | LaxMonEndofunctor : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> (f : obj -> obj) -> Type
41 | LaxMonEndofunctor cat ten i = LaxMonFunctor cat ten i cat ten i
53 | interface LaxMonFunctor cat ten i cat' ten' i' f => MonFunctor
54 | (0 cat : Hom obj) (0 ten : obj -> obj -> obj) (0 i : obj)
55 | (0 cat' : Hom obj') (0 ten' : obj' -> obj' -> obj') (0 i' : obj')
56 | (0 f : obj -> obj') | cat,ten,cat',ten',f where
57 | constructor MkMonFunctor
61 | fjoin' : {a,b : _} -> cat' (f (a `ten` b)) (f a `ten'` f b)
65 | funit' : cat' (f i) i'
72 | public export %inline
73 | MonEndofunctor : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> (f : obj -> obj) -> Type
74 | MonEndofunctor cat ten i = MonFunctor cat ten i cat ten i
95 | interface CatFunctor cat cat f => StrongFunctor
97 | (0 ten : obj -> obj -> obj)
98 | (0 f : obj -> obj) | cat,ten,f where
99 | constructor MkStrongFunctor
101 | strongl : {a,b : _} -> cat (a `ten` f b) (f $
a `ten` b)
103 | strongr : {a,b : _} -> cat (f a `ten` b) (f $
a `ten` b)
121 | interface CatFunctor cat cat f => CostrongFunctor
123 | (0 ten : obj -> obj -> obj)
124 | (0 f : obj -> obj) | cat,ten,f where
125 | constructor MkCostrongFunctor
127 | costrongl : {a,b : _} -> cat (f $
a `ten` b) (a `ten` f b)
129 | costrongr : {a,b : _} -> cat (f $
a `ten` b) (f a `ten` b)
136 | namespace LaxMonFunctor
138 | [Id] {ten,i : _} -> Category cat => LaxMonFunctor cat ten i cat ten i Prelude.id
139 | using CatFunctor.Id where
143 | namespace MonFunctor
145 | [Id] {ten,i : _} -> Category cat => MonFunctor cat ten i cat ten i Prelude.id
146 | using LaxMonFunctor.Id where
150 | namespace StrongFunctor
152 | [Id] {ten : _} -> Category cat => StrongFunctor cat ten Prelude.id
153 | using CatFunctor.Id where
157 | namespace CostrongFunctor
159 | [Id] {ten : _} -> Category cat => CostrongFunctor cat ten Prelude.id
160 | using CatFunctor.Id where
169 | namespace LaxMonFunctor
173 | [MorFromApplicative] Applicative f => LaxMonFunctor Morphism Pair () Morphism Pair () f
174 | using CatFunctor.MorFromFunctor where
175 | fjoin = Mor $
\(x,y) => (,) <$> x <*> y
176 | funit = Mor $
const $
pure ()
181 | [FuncFromApplicative] Applicative f => LaxMonFunctor (~~>) Pair () (~~>) Pair () f
182 | using CatFunctor.FuncFromFunctor where
183 | fjoin (x,y) = (,) <$> x <*> y
184 | funit = const $
pure ()
186 | namespace StrongFunctor
190 | [MorFromFunctor] Functor f => StrongFunctor Morphism Pair f
191 | using CatFunctor.MorFromFunctor where
192 | strongl = Mor $
\(x,y) => map (x,) y
193 | strongr = Mor $
\(x,y) => map (,y) x
198 | [FuncFromFunctor] Functor m => StrongFunctor (~~>) Pair m
199 | using CatFunctor.FuncFromFunctor where
200 | strongl (x,y) = map (x,) y
201 | strongr (x,y) = map (,y) x
206 | [MorFromApplicative] Applicative f => Bitraversable ten => StrongFunctor Morphism ten f
207 | using CatFunctor.MorFromFunctor where
208 | strongl = Mor $
bitraverse pure id
209 | strongr = Mor $
bitraverse id pure
214 | [FuncFromApplicative] Applicative f => Bitraversable ten => StrongFunctor (~~>) ten f
215 | using CatFunctor.FuncFromFunctor where
216 | strongl = bitraverse pure id
217 | strongr = bitraverse id pure