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 | SymmetricFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
 88 |                   MonSymmetric cat'.hom ten i => MonSymmetric (FunCat cat cat') (FunProd ten) (FunUnit i)
 89 | SymmetricFunCat {cat'=cat'@(MkCategoryR{})} = MkMonSymmetric @{BraidedFunCat} (permuteDefault @{BraidedFunCat})
 90 |
 91 | public export %hint
 92 | CartesianFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
 93 |                   Cartesian cat'.hom ten i => Cartesian (FunCat cat cat') (FunProd ten) (FunUnit i)
 94 | CartesianFunCat {cat'=cat'@(MkCategoryR{})} = MkCartesian @{MonoidalFunCat} projl_ projr_ prod_ split_ elim_
 95 |   where
 96 |     projl_ : {f,g : _} -> NatTransR {cat'} (FunProd ten f g) f
 97 |     projl_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR projl
 98 |
 99 |     projr_ : {f,g : _} -> NatTransR {cat'} (FunProd ten f g) g
100 |     projr_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR projr
101 |
102 |     prod_ : {f,g,g' : _} -> NatTransR {cat'} f g -> NatTransR f g' -> NatTransR f (FunProd ten g g')
103 |     prod_ {f=MkFunctorR{},g=MkFunctorR{},g'=MkFunctorR{}} (MkNatTransR tr) (MkNatTransR tr') =
104 |       MkNatTransR $ prod tr tr'
105 |
106 |     split_ : {f : _} -> NatTransR {cat'} f (FunProd ten f f)
107 |     split_ {f=MkFunctorR{}} = MkNatTransR split
108 |
109 |     elim_ : {f : _} -> NatTransR {cat'} f (FunUnit i)
110 |     elim_ {f=MkFunctorR{}} = MkNatTransR $ elim {ten}
111 |
112 | public export %hint
113 | CocartesianFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
114 |                     Cocartesian cat'.hom ten i => Cocartesian (FunCat cat cat') (FunProd ten) (FunUnit i)
115 | CocartesianFunCat {cat'=cat'@(MkCategoryR{})} = MkCocartesian @{MonoidalFunCat} injl_ injr_ coprod_ merge_ intro_
116 |   where
117 |     injl_ : {f,g : _} -> NatTransR {cat'} f (FunProd ten f g)
118 |     injl_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR injl
119 |
120 |     injr_ : {f,g : _} -> NatTransR {cat'} g (FunProd ten f g)
121 |     injr_ {f=MkFunctorR{},g=MkFunctorR{}} = MkNatTransR injr
122 |
123 |     coprod_ : {f,f',g : _} -> NatTransR {cat'} f g -> NatTransR f' g -> NatTransR (FunProd ten f f') g
124 |     coprod_ {f=MkFunctorR{},f'=MkFunctorR{},g=MkFunctorR{}} (MkNatTransR tr) (MkNatTransR tr') =
125 |       MkNatTransR $ coprod tr tr'
126 |
127 |     merge_ : {f : _} -> NatTransR {cat'} (FunProd ten f f) f
128 |     merge_ {f=MkFunctorR{}} = MkNatTransR merge
129 |
130 |     intro_ : {f : _} -> NatTransR {cat'} (FunUnit i) f
131 |     intro_ {f=MkFunctorR{}} = MkNatTransR $ intro {ten}
132 |
133 | public export %hint
134 | TracedFunCat : {cat' : _} -> {ten : cat'.obj -> cat'.obj -> cat'.obj} -> {i : cat'.obj} ->
135 |                Traced cat'.hom ten i => Traced (FunCat cat cat') (FunProd ten) (FunUnit i)
136 | TracedFunCat {cat'=cat'@(MkCategoryR{})} = MkTraced @{MonoidalFunCat} tracel_ tracer_
137 |   where
138 |     tracel_ : {f,g,h : _} -> NatTransR {cat'} (FunProd ten f g) (FunProd ten f h) -> NatTransR g h
139 |     tracel_ {f=MkFunctorR{},g=MkFunctorR{},h=MkFunctorR{}} (MkNatTransR tr) = MkNatTransR $ tracel tr
140 |
141 |     tracer_ : {f,g,h : _} -> NatTransR {cat'} (FunProd ten f h) (FunProd ten g h) -> NatTransR f g
142 |     tracer_ {f=MkFunctorR{},g=MkFunctorR{},h=MkFunctorR{}} (MkNatTransR tr) = MkNatTransR $ tracer tr
143 |
144 |
145 | ------------------------------------------------------------
146 | -- Record Style
147 | ------------------------------------------------------------
148 |
149 | namespace CategoryR
150 |   public export
151 |   FunCat : (cat,cat' : CategoryR) -> CategoryR
152 |   FunCat cat cat' = MkCategoryR (FunCat cat cat')
153 |
154 | namespace MonoidalR
155 |   public export
156 |   FunCat : (cat : CategoryR) -> (cat' : MonoidalR) -> MonoidalR
157 |   FunCat cat cat'@(MkMonoidalR {}) =
158 |     MkMonoidalR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
159 |       {impl = MonoidalFunCat}
160 |
161 | namespace BraidedR
162 |   public export
163 |   FunCat : (cat : CategoryR) -> (cat' : BraidedR) -> BraidedR
164 |   FunCat cat cat'@(MkBraidedR {}) =
165 |     MkBraidedR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
166 |       {impl = BraidedFunCat}
167 |
168 | namespace SymmetricR
169 |   public export
170 |   FunCat : (cat : CategoryR) -> (cat' : SymmetricR) -> SymmetricR
171 |   FunCat cat cat'@(MkSymmetricR {}) =
172 |     MkSymmetricR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
173 |       {impl = SymmetricFunCat}
174 |
175 | namespace CartesianR
176 |   public export
177 |   FunCat : (cat : CategoryR) -> (cat' : CartesianR) -> CartesianR
178 |   FunCat cat cat'@(MkCartesianR {}) =
179 |     MkCartesianR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
180 |       {impl = CartesianFunCat}
181 |
182 | namespace CocartesianR
183 |   public export
184 |   FunCat : (cat : CategoryR) -> (cat' : CocartesianR) -> CocartesianR
185 |   FunCat cat cat'@(MkCocartesianR {}) =
186 |     MkCocartesianR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
187 |       {impl = CocartesianFunCat}
188 |
189 | namespace TracedR
190 |   public export
191 |   FunCat : (cat : CategoryR) -> (cat' : TracedR) -> TracedR
192 |   FunCat cat cat'@(MkTracedR {}) =
193 |     MkTracedR (FunCat cat cat'.categoryR) (FunProd cat'.tensor) (FunUnit cat'.unit)
194 |       {impl = TracedFunCat}
195 |