
   0 | module Data.CT.Functor.Instances
   1 | 
   2 | import Data.CT.Category.Definition
   3 | import Data.CT.Category.Instances
   4 | import Data.CT.Functor.Definition
   5 | 
   6 | import Data.Vect
   7 | import Data.Container.Base
   8 | import Data.Container.Additive
   9 | 
  10 | public export
  11 | id : Functor c c
  12 | id = MkFunctor id id
  13 | 
  14 | ||| Functor Type -> Cat^op
  15 | public export
  16 | IndCat : (c : Cat) -> Type
  17 | IndCat c = Functor c (opCat Cat)
  18 | 
  19 | public export
  20 | Const : {c : Cat} -> IndCat c
  21 | Const = MkFunctor (\_ => c) (\_ => id)
  22 | 
  23 | namespace Fam
  24 |   public export
  25 |   FamObj : {c : Cat} -> (a : Type) -> Cat
  26 |   FamObj a = MkCat (a -> c.Obj) (\a', b' => (x : a) -> c.Hom (a' x) (b' x))
  27 | 
  28 |   public export
  29 |   FamMor : {c : Cat} ->
  30 |     {0 x, y : Type} -> (x -> y) -> Functor (FamObj {c=c} y) (FamObj {c=c} x)
  31 |   FamMor f = MkFunctor (. f) (\j, xx => j (f xx))
  32 | 
  33 |   ||| Functor Type -> Cat^op, we will mostly instantiate this for `c=TypeCat`
  34 |   public export
  35 |   FamIndCat : {c : Cat} -> IndCat TypeCat
  36 |   FamIndCat = MkFunctor (\a => FamObj {c=c} a) FamMor
  37 | 
  38 | ||| Functor which projects the forward part of a dependent lens
  39 | public export
  40 | Base : Functor DLens TypeCat
  41 | Base = MkFunctor Shp (.fwd)
  42 | 
  43 | ||| DLens -> Type -> Cat^op
  44 | public export
  45 | FamDLens : {c : Cat} -> IndCat DLens
  46 | FamDLens = composeFunctors Base (FamIndCat {c=c})
  47 | 
  48 | ||| Functor which projects out the forward part of an additive dependent lens
  49 | public export
  50 | AddBase : Functor AddDLens TypeCat
  51 | AddBase = MkFunctor (.Shp) (.fwd)
  52 | 
  53 | public export
  54 | FamAddDLens : {c : Cat} -> IndCat AddDLens
  55 | FamAddDLens = composeFunctors AddBase (FamIndCat {c=c})
  56 | 
  57 | -- need to check everything from here onwards
  58 | 
  59 | namespace Type
  60 |   public export
  61 |   IndexedType : Type -> Type
  62 |   IndexedType a = a -> Type
  63 |   
  64 |   public export
  65 |   TypeDPair : {a : Type} -> IndexedType a -> Type
  66 |   TypeDPair fam = (x : a ** fam x)
  67 | 
  68 |   public export
  69 |   TypeDFun : {a : Type} -> IndexedType a -> Type
  70 |   TypeDFun fam = (x : a) -> fam x
  71 | 
  72 | namespace Cont
  73 |   ||| TODO probably name clash with other "Indexed container"
  74 |   public export
  75 |   IndexedCont : Cont -> Type
  76 |   IndexedCont c = c.Shp -> Cont
  77 |   
  78 |   public export
  79 |   ContDPair : {a : Cont} -> IndexedCont a -> Cont
  80 |   ContDPair a' = ((x ** t) : DPair a.Shp (Shp . a')) !> (a' x).Pos t
  81 | 
  82 |   public export
  83 |   ContProbDPair : {a : Cont} -> IndexedCont a -> Cont
  84 |   ContProbDPair a' = (((x, d) ** t) : DPair (a.Shp, Double) (Shp . a' . fst)) !>
  85 |     (a' x).Pos t
  86 | 
  87 | namespace AddCont
  88 |   public export
  89 |   IndexedAddCont : AddCont -> Type
  90 |   IndexedAddCont c = c.Shp -> AddCont
  91 | 
  92 |   public export
  93 |   AddContDPair : {a : AddCont} -> IndexedAddCont a -> AddCont
  94 |   AddContDPair a' = MkAddCont
  95 |     (DPair a.Shp (\x => (a' x).Shp))
  96 |     (\(x ** x') => (a' x).Pos x')
  97 | 
  98 | 
  99 |   public export
 100 |   AddContDFunFinite : {n : Nat} -> (Fin n -> AddCont) -> AddCont
 101 |   AddContDFunFinite {n = 0} i = UnitCont
 102 |   AddContDFunFinite {n = (S k)} i = i 0 >*< AddContDFunFinite (i . FS)
 103 | 
 104 |   public export
 105 |   indexShp : {n : Nat} -> {i : Fin n -> AddCont} ->
 106 |     (j : Fin n) ->
 107 |     (AddContDFunFinite i).Shp -> (i j).Shp
 108 |   indexShp {n = (S k)} FZ (s, _) = s
 109 |   indexShp {n = (S k)} {i} (FS y) (_, ss) = indexShp {i=i . FS} y ss
 110 | 
 111 |   public export
 112 |   injectPos : {n : Nat} -> {f : Fin n -> AddCont} ->
 113 |     (j : Fin n) -> (bp : (AddContDFunFinite f).Shp) ->
 114 |     (f j).PosSet (indexShp {i=f} j bp) ->
 115 |     (AddContDFunFinite f).PosSet bp
 116 |   injectPos {n = S k} FZ (p, rest) g =
 117 |     (g, (AddContDFunFinite (f . FS)).Zero rest)
 118 |   injectPos {n = S k} {f} (FS j) (p, rest) g =
 119 |     ((f FZ).Zero p, injectPos {f=f . FS} j rest g)
 120 | 
 121 |   ||| Sections of a finite family inside the choice effect: forward the graph
 122 |   ||| of the section, backward the free-monoid counit at the coprojections
 123 |   public export
 124 |   graph : {n : Nat} -> {br : Vect n AddCont} ->
 125 |     AddContDFunFinite (\i => index i br) =%+> Vect n >-+@ Coproduct br
 126 |   graph = !%+ \s =>
 127 |     (() <| (\i => (i ** indexShp {i = \i => index i br} i s)) **
 128 |      fromGenerators {y = (AddContDFunFinite (\i => index i br)).Pos s}
 129 |        (\(i ** g) => injectPos {f = \i => index i br} i s g))
 130 | 
 131 |   public export
 132 |   AddContDFunction : {a : AddCont} -> IndexedAddCont a -> AddCont
 133 |   AddContDFunction a' = MkAddCont
 134 |     ((x : a.Shp) -> (a' x).Shp)
 135 |     (\s => (((x : a.Shp) -> (a' x).PosSet (s x)) ** MkComMonoid
 136 |       (\l, r => \x => (a' x).Plus (s x) (l x) (r x))
 137 |       (\x => (a' x).Zero (s x))))
 138 | 
 139 | -- public export
 140 | -- ContDPair : (c : Cont) -> IndexedCont c -> Cont
 141 | -- ContDPair c fam = 
 142 | --   (st : (s : c.Shp ** (fam s).Shp)) !> 
 143 | --   Either (c.Pos (fst st)) ((fam (fst st)).Pos (snd st))
 144 | 
 145 | -- Simpler version: just the family positions (no base positions)
 146 | -- This corresponds to the "total space" of a display map
 147 | public export
 148 | ContDPairSimple : (c : Cont) -> IndexedCont c -> Cont
 149 | ContDPairSimple c fam = 
 150 |   (st : (s : c.Shp ** (fam s).Shp)) !> 
 151 |   (fam (fst st)).Pos (snd st)
 152 | 
 153 | --------------------------------------------------------------------------------
 154 | -- DEPENDENT PRODUCT in Poly (Π-types) — MORE SUBTLE
 155 | --
 156 | -- Π-types do NOT always exist in Poly. When they do exist:
 157 | --   - Shapes: Π(s : S). (fam s).Shp     -- sections of the family
 158 | --   - Positions: Σ(s : S). Σ(p : P s). (fam s).Pos (f s)
 159 | --
 160 | -- This only type-checks when S is "small enough" that we can form Π over it.
 161 | --------------------------------------------------------------------------------
 162 | 
 163 | public export
 164 | ContDFun : (c : Cont) -> IndexedCont c -> Cont
 165 | ContDFun c fam = 
 166 |   (f : ((s : c.Shp) -> (fam s).Shp)) !> 
 167 |   (s : c.Shp ** (p : c.Pos s ** (fam s).Pos (f s)))
 168 | 
 169 | --------------------------------------------------------------------------------
 170 | -- EXAMPLES
 171 | --------------------------------------------------------------------------------
 172 | 
 173 | -- Constant family: assigns the same container to every shape
 174 | public export
 175 | constFam : {c : Cont} -> Cont -> IndexedCont c
 176 | constFam d = \_ => d
 177 | 
 178 | -- Trivial family: assigns the unit container (one shape, no positions) to every shape
 179 | public export
 180 | trivialFam : {c : Cont} -> IndexedCont c
 181 | trivialFam = \_ => ((_ : ()) !> Void)
 182 | 
 183 | -- Family that assigns Bool shapes with no positions
 184 | public export
 185 | boolFam : {c : Cont} -> IndexedCont c
 186 | boolFam = \_ => ((_ : Bool) !> Void)