0 | ||| This module defines the functor category between two categories,
  1 | ||| `FunCat C D`, traditionally written `[C, D]`. Its morphisms are
  2 | ||| natural transformations between parallel functors.
  3 | module Control.Category.Instances.FunCat
  4 |
  5 | import Control.Category
  6 | import Control.Category.Instances.One
  7 | import Control.Category.Instances.Prod
  8 | import Control.Category.Records
  9 |
 10 | %default total
 11 |
 12 | ||| The functor category between `cat` and `cat'`.
 13 | |||
 14 | ||| This category doesn't play very nicely with Idris's interface
 15 | ||| resolution. Consider using the record-style definitions below.
 16 | public export
 17 | FunCat : (cat, cat' : CategoryR) -> Hom (FunctorR cat cat')
 18 | FunCat _ _ = NatTransR
 19 |
 20 | public export
 21 | FunProd : {cat' : _} -> (ten : cat'.obj -> cat'.obj -> cat'.obj) -> CatEndoBifunctor cat'.hom ten =>
 22 |             (f,g : FunctorR cat cat') -> FunctorR cat cat'
 23 | FunProd {cat'=cat'@(MkCategoryR{})} ten f@(MkFunctorR _) g@(MkFunctorR _) =
 24 |   MkFunctorR (\x => ten (f.fun x) (g.fun x))
 25 |     {impl = MkCatFunctor $ \x => bimap (f.map x) (g.map x)}
 26 |
 27 | public export
 28 | FunUnit : {cat' : _} -> (i : cat'.obj) -> FunctorR cat cat'
 29 | FunUnit i = MkFunctorR (const i) {impl = Const @{cat'.impl}}
 30 |
 31 |
 32 | ------------------------------------------------------------
 33 | -- Interface Style
 34 | ------------------------------------------------------------
 35 |
 36 | public export
 37 | {cat' : _} -> Category (FunCat cat cat') where
 38 |   id = NatTransR.id
 39 |   (.) = NatTransR.(.)
 40 |
 41 | public export %hint
 42 | [BifunctorFunProd] {cat' : _} -> {0 ten : cat'.obj -> cat'.obj -> cat'.obj} ->
 43 |     CatBifunctor cat'.hom cat'.hom cat'.hom ten =>
 44 |     CatBifunctor (FunCat cat cat')
 45 |                  (FunCat cat cat')
 46 |                  (FunCat cat cat') (FunProd ten) where
 47 |   bimap {cat'=cat'@(MkCategoryR{}),
 48 |     a=MkFunctorR{},a'=MkFunctorR{},b=MkFunctorR{},b'=MkFunctorR{}}
 49 |     (MkNatTransR tr) (MkNatTransR tr') = MkNatTransR $ bimap tr tr'
 50 |
 51 | public export %hint
 52 | MonoidalFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
 53 |                   Monoidal cat'.hom ten i => Monoidal (FunCat cat cat') (FunProd ten) (FunUnit i)
 54 | MonoidalFunCat {cat'=cat'@(MkCategoryR{})} =
 55 |   MkMonoidal @{%search} @{BifunctorFunProd} assoc_ assoc'_ unitl_ unitl'_ unitr_ unitr'_
 56 |   where
 57 |     assoc_ : {f,g,h : _} -> NatTransR {cat'} (FunProd ten (FunProd ten f g) h) (FunProd ten f (FunProd ten g h))
 58 |     assoc_ {f=MkFunctorR{},g=MkFunctorR{},h=MkFunctorR{}} = MkNatTransR assoc
 59 |
 60 |     assoc'_ : {f,g,h : _} -> NatTransR {cat'} (FunProd ten f (FunProd ten g h)) (FunProd ten (FunProd ten f g) h)
 61 |     assoc'_ {f=MkFunctorR{},g=MkFunctorR{},h=MkFunctorR{}} = MkNatTransR assoc'
 62 |
 63 |     unitl_ : {f : _} -> NatTransR {cat'} (FunProd ten (FunUnit i) f) f
 64 |     unitl_ {f=MkFunctorR{}} = MkNatTransR unitl
 65 |
 66 |     unitl'_ : {f : _} -> NatTransR {cat'} f (FunProd ten (FunUnit i) f)
 67 |     unitl'_ {f=MkFunctorR{}} = MkNatTransR unitl'
 68 |
 69 |     unitr_ : {f : _} -> NatTransR {cat'} (FunProd ten f (FunUnit i)) f
 70 |     unitr_ {f=MkFunctorR{}} = MkNatTransR unitr
 71 |
 72 |     unitr'_ : {f : _} -> NatTransR {cat'} f (FunProd ten f (FunUnit i))
 73 |     unitr'_ {f=MkFunctorR{}} = MkNatTransR unitr'
 74 |
 75 | public export %hint
 76 | BraidedFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
 77 |                   Braided cat'.hom ten i => Braided (FunCat cat cat') (FunProd ten) (FunUnit i)
 78 | BraidedFunCat {cat'=cat'@(MkCategoryR{})} = MkBraided @{MonoidalFunCat} braid_ braid'_
 79 |   where
 80 |     braid_ : {f,g : _} -> NatTransR {cat'} (FunProd ten f g) (FunProd ten g f)
 81 |     braid_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR braid
 82 |
 83 |     braid'_ : {f,g : _} -> NatTransR {cat'} (FunProd ten g f) (FunProd ten f g)
 84 |     braid'_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR braid'
 85 |
 86 | public export %hint
 87 | CartesianFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
 88 |                   Cartesian cat'.hom ten i => Cartesian (FunCat cat cat') (FunProd ten) (FunUnit i)
 89 | CartesianFunCat {cat'=cat'@(MkCategoryR{})} = MkCartesian @{MonoidalFunCat} projl_ projr_ prod_ split_ elim_
 90 |   where
 91 |     projl_ : {f,g : _} -> NatTransR {cat'} (FunProd ten f g) f
 92 |     projl_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR projl
 93 |
 94 |     projr_ : {f,g : _} -> NatTransR {cat'} (FunProd ten f g) g
 95 |     projr_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR projr
 96 |
 97 |     prod_ : {f,g,g' : _} -> NatTransR {cat'} f g -> NatTransR f g' -> NatTransR f (FunProd ten g g')
 98 |     prod_ {f=MkFunctorR{},g=MkFunctorR{},g'=MkFunctorR{}} (MkNatTransR tr) (MkNatTransR tr') =
 99 |       MkNatTransR $ prod tr tr'
100 |
101 |     split_ : {f : _} -> NatTransR {cat'} f (FunProd ten f f)
102 |     split_ {f=MkFunctorR{}} = MkNatTransR split
103 |
104 |     elim_ : {f : _} -> NatTransR {cat'} f (FunUnit i)
105 |     elim_ {f=MkFunctorR{}} = MkNatTransR $ elim {ten}
106 |
107 | public export %hint
108 | CocartesianFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
109 |                     Cocartesian cat'.hom ten i => Cocartesian (FunCat cat cat') (FunProd ten) (FunUnit i)
110 | CocartesianFunCat {cat'=cat'@(MkCategoryR{})} = MkCocartesian @{MonoidalFunCat} injl_ injr_ coprod_ merge_ intro_
111 |   where
112 |     injl_ : {f,g : _} -> NatTransR {cat'} f (FunProd ten f g)
113 |     injl_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR injl
114 |
115 |     injr_ : {f,g : _} -> NatTransR {cat'} g (FunProd ten f g)
116 |     injr_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR injr
117 |
118 |     coprod_ : {f,f',g : _} -> NatTransR {cat'} f g -> NatTransR f' g -> NatTransR (FunProd ten f f') g
119 |     coprod_ {f=MkFunctorR{},f'=MkFunctorR{},g=MkFunctorR{}} (MkNatTransR tr) (MkNatTransR tr') =
120 |       MkNatTransR $ coprod tr tr'
121 |
122 |     merge_ : {f : _} -> NatTransR {cat'} (FunProd ten f f) f
123 |     merge_ {f=MkFunctorR{}} = MkNatTransR merge
124 |
125 |     intro_ : {f : _} -> NatTransR {cat'} (FunUnit i) f
126 |     intro_ {f=MkFunctorR{}} = MkNatTransR $ intro {ten}
127 |
128 | public export %hint
129 | TracedFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
130 |                Traced cat'.hom ten i => Traced (FunCat cat cat') (FunProd ten) (FunUnit i)
131 | TracedFunCat {cat'=cat'@(MkCategoryR{})} = MkTraced @{MonoidalFunCat} tracel_ tracer_
132 |   where
133 |     tracel_ : {f,g,h : _} -> NatTransR {cat'} (FunProd ten f g) (FunProd ten f h) -> NatTransR g h
134 |     tracel_ {f=MkFunctorR{},g=MkFunctorR{},h=MkFunctorR{}} (MkNatTransR tr) = MkNatTransR $ tracel tr
135 |
136 |     tracer_ : {f,g,h : _} -> NatTransR {cat'} (FunProd ten f h) (FunProd ten g h) -> NatTransR f g
137 |     tracer_ {f=MkFunctorR{},g=MkFunctorR{},h=MkFunctorR{}} (MkNatTransR tr) = MkNatTransR $ tracer tr
138 |
139 |
140 | ------------------------------------------------------------
141 | -- Record Style
142 | ------------------------------------------------------------
143 |
144 | namespace CategoryR
145 |   public export
146 |   FunCat : (cat,cat' : CategoryR) -> CategoryR
147 |   FunCat cat cat' = MkCategoryR (FunCat cat cat')
148 |
149 | namespace MonoidalR
150 |   public export
151 |   FunCat : (cat : CategoryR) -> (cat' : MonoidalR) -> MonoidalR
152 |   FunCat cat cat'@(MkMonoidalR {}) =
153 |     MkMonoidalR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
154 |       {impl = MonoidalFunCat}
155 |
156 | namespace BraidedR
157 |   public export
158 |   FunCat : (cat : CategoryR) -> (cat' : BraidedR) -> BraidedR
159 |   FunCat cat cat'@(MkBraidedR {}) =
160 |     MkBraidedR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
161 |       {impl = BraidedFunCat}
162 |
163 | namespace CartesianR
164 |   public export
165 |   FunCat : (cat : CategoryR) -> (cat' : CartesianR) -> CartesianR
166 |   FunCat cat cat'@(MkCartesianR {}) =
167 |     MkCartesianR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
168 |       {impl = CartesianFunCat}
169 |
170 | namespace CocartesianR
171 |   public export
172 |   FunCat : (cat : CategoryR) -> (cat' : CocartesianR) -> CocartesianR
173 |   FunCat cat cat'@(MkCocartesianR {}) =
174 |     MkCocartesianR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
175 |       {impl = CocartesianFunCat}
176 |
177 | namespace TracedR
178 |   public export
179 |   FunCat : (cat : CategoryR) -> (cat' : TracedR) -> TracedR
180 |   FunCat cat cat'@(MkTracedR {}) =
181 |     MkTracedR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
182 |       {impl = TracedFunCat}
183 |