0 | module Control.Category.Records.Functor
 1 |
 2 | import Control.Category
 3 | import Control.Category.Records.Category
 4 |
 5 | %default total
 6 | %prefix_record_projections off
 7 |
 8 | ||| A *functor* is a mapping between categories that preserves their
 9 | ||| structure.
10 | |||
11 | ||| See `CatFunctor` for required laws.
12 | public export
13 | record FunctorR (cat,cat' : CategoryR) where
14 |   constructor MkFunctorR
15 |   fun : cat.obj -> cat'.obj
16 |   {auto impl : CatFunctor cat.hom cat'.hom fun}
17 |
18 | ||| A type synonym for an *endofunctor*, a functor from a category to
19 | ||| itself.
20 | public export
21 | EndofunctorR : (cat : CategoryR) -> Type
22 | EndofunctorR cat = FunctorR cat cat
23 |
24 |
25 | namespace FunctorR
26 |   ||| Convert this into a `FunctorR`.
27 |   public export %inline
28 |   (.functorR) : (rec : FunctorR cat cat') -> FunctorR cat cat'
29 |   (.functorR) = id
30 |
31 |   ||| Apply the functor to a morphism in `cat`, translating it into `cat'`.
32 |   public export %inline
33 |   (.map) : (rec : FunctorR cat cat') -> {a,b : _} ->
34 |            cat.hom a b -> cat'.hom (rec.fun a) (rec.fun b)
35 |   (.map) rec = map @{rec.impl}
36 |
37 |
38 | ||| A *bifunctor* is a binary functor, i.e. a functor that maps two
39 | ||| categories to one.
40 | |||
41 | ||| See `CatBifunctor` for required laws.
42 | public export
43 | record BifunctorR (catA,catB,cat' : CategoryR) where
44 |   constructor MkBifunctorR
45 |   fun : catA.obj -> catB.obj -> cat'.obj
46 |   {auto impl : CatBifunctor catA.hom catB.hom cat'.hom fun}
47 |
48 | ||| See `Binoidal`.
49 | public export
50 | BinoidalR : (catA,catB,cat' : CategoryR) -> Type
51 | BinoidalR = BifunctorR
52 |
53 | ||| A type synonym for an *endo-bifunctor*, a bifunctor from a category
54 | ||| to itself.
55 | public export
56 | EndoBifunctorR : (cat : CategoryR) -> Type
57 | EndoBifunctorR cat = BifunctorR cat cat cat
58 |
59 | ||| See `Binoidal`.
60 | public export
61 | EndoBinoidalR : (cat : CategoryR) -> Type
62 | EndoBinoidalR = EndoBifunctorR
63 |
64 | namespace BifunctorR
65 |   ||| Apply the bifunctor to morphism in `catA` and `catB`, translating
66 |   ||| them into a combined morphism in `cat'`.
67 |   public export %inline
68 |   (.bimap) : (rec : BifunctorR catA catB cat') -> {a,a',b,b' : _} ->
69 |              catA.hom a b -> catB.hom a' b' -> cat'.hom (rec.fun a a') (rec.fun b b')
70 |   (.bimap) rec = bimap @{rec.impl}
71 |
72 |   ||| Apply a morphism to a bifunctor only on the left.
73 |   public export %inline
74 |   (.mapl) : {catB : _} -> (rec : BifunctorR catA catB cat') -> {a,b,c : _} ->
75 |             catA.hom a b -> cat'.hom (rec.fun a c) (rec.fun b c)
76 |   (.mapl) rec = mapl @{rec.impl} @{catB.impl}
77 |
78 |   ||| Apply a morphism to a bifunctor only on the right.
79 |   public export %inline
80 |   (.mapr) : {catA : _} -> (rec : BifunctorR catA catB cat') -> {a,b,c : _} ->
81 |             catB.hom a b -> cat'.hom (rec.fun c a) (rec.fun c b)
82 |   (.mapr) rec = mapr @{rec.impl} @{catA.impl}
83 |
84 |   -- Functor Projections
85 |
86 |   ||| Convert a bifunctor (or binoidal functor) into its left functor.
87 |   public export %inline
88 |   (.left) : {catB : _} -> (rec : BifunctorR catA catB cat') ->
89 |             (l : catB.obj) -> FunctorR catA cat'
90 |   (.left) {catB=MkCategoryR {}} (MkBifunctorR {} {fun,impl}) l =
91 |     MkFunctorR (`fun` l) {impl = Left @{impl}}
92 |
93 |   ||| Convert a bifunctor (or binoidal functor) into its right functor.
94 |   public export %inline
95 |   (.right) : {catA : _} -> (rec : BifunctorR catA catB cat') ->
96 |              (l : catA.obj) -> FunctorR catB cat'
97 |   (.right) {catA=MkCategoryR {}} (MkBifunctorR {} {fun,impl}) l =
98 |     MkFunctorR (l `fun`) {impl = Right @{impl}}
99 |