0 | ||| This module defines endofunctors in the category of profunctors `[Idrᵒᵖ * Idr, Idr]`,
 1 | ||| along with adjunctions of those functors.
 2 | ||| Examples of these functors include `Yoneda`, `Pastro`, `Closure`, etc.
 3 | module Data.Profunctor.Functor
 4 |
 5 | import Data.Profunctor.Types
 6 |
 7 | %default total
 8 |
 9 |
10 | ||| An endofunctor in the category of profunctors.
11 | |||
12 | ||| Laws:
13 | ||| * `promap id = id`
14 | ||| * `promap g . promap f = promap (g . f)`
15 | public export
16 | interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> k -> k' -> Type) where
17 |   ||| Lift a transformation between profunctors into the functor `t`.
18 |   promap : Profunctor p => p :-> q -> t p :-> t q
19 |
20 |
21 | ||| A monad in the category of profunctors.
22 | ||| 
23 | ||| Laws:
24 | ||| * `projoin . proreturn ≡ id`
25 | ||| * `projoin . promap proreturn ≡ id`
26 | ||| * `projoin . projoin ≡ projoin . promap projoin`
27 | public export
28 | interface ProfunctorFunctor t =>
29 |     ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
30 |   propure : Profunctor p => p :-> t p
31 |   projoin : Profunctor p => t (t p) :-> t p
32 |
33 | ||| A comonad in the category of profunctors.
34 | |||
35 | ||| Laws:
36 | ||| * `proextract . produplicate ≡ id`
37 | ||| * `promap proextract . produplicate ≡ id`
38 | ||| * `produplicate . produplicate ≡ promap produplicate . produplicate`
39 | public export
40 | interface ProfunctorFunctor t =>
41 |     ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
42 |   proextract : Profunctor p => t p :-> p
43 |   produplicate : Profunctor p => t p :-> t (t p)
44 |
45 | ||| An adjunction between endofunctors in the category of profunctors.
46 | |||
47 | ||| Laws:
48 | ||| * `counit . promap unit ≡ id`
49 | ||| * `promap counit . unit ≡ id`
50 | public export
51 | interface (ProfunctorFunctor l, ProfunctorFunctor r) =>
52 |     ProfunctorAdjunction (0 l, r : (Type -> Type -> Type) -> Type -> Type -> Type) | l, r where
53 |   prounit   : Profunctor p => p :-> r (l p)
54 |   procounit : Profunctor p => l (r p) :-> p
55 |