
   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.Container.Base
   7 | import Data.Container.Additive
   8 | 
   9 | public export
  10 | id : Functor c c
  11 | id = MkFunctor id id
  12 | 
  13 | ||| Functor Type -> Cat^op
  14 | public export
  15 | IndCat : (c : Cat) -> Type
  16 | IndCat c = Functor c (opCat Cat)
  17 | 
  18 | public export
  19 | Const : {c : Cat} -> IndCat c
  20 | Const = MkFunctor (\_ => c) (\_ => id)
  21 | 
  22 | namespace Fam
  23 |   public export
  24 |   FamObj : {c : Cat} -> (a : Type) -> Cat
  25 |   FamObj a = MkCat (a -> c.Obj) (\a', b' => (x : a) -> c.Hom (a' x) (b' x))
  26 | 
  27 |   public export
  28 |   FamMor : {c : Cat} ->
  29 |     {x, y : Type} -> (x -> y) -> Functor (FamObj {c=c} y) (FamObj {c=c} x)
  30 |   FamMor f = MkFunctor (. f) (\j, xx => j (f xx))
  31 | 
  32 |   ||| Functor Type -> Cat^op, we will mostly instantiate this for `c=TypeCat`
  33 |   public export
  34 |   FamIndCat : {c : Cat} -> IndCat TypeCat
  35 |   FamIndCat = MkFunctor (\a => FamObj {c=c} a) FamMor
  36 | 
  37 | ||| Functor which projects the forward part of a dependent lens
  38 | public export
  39 | Base : Functor DLens TypeCat
  40 | Base = MkFunctor Shp (.fwd)
  41 | 
  42 | ||| DLens -> Type -> Cat^op
  43 | public export
  44 | FamDLens : {c : Cat} -> IndCat DLens
  45 | FamDLens = composeFunctors Base (FamIndCat {c=c})
  46 | 
  47 | ||| Functor which projects out the forward part of an additive dependent lens
  48 | public export
  49 | AddBase : Functor AddDLens TypeCat
  50 | AddBase = MkFunctor (.Shp) (.fwd)
  51 | 
  52 | public export
  53 | FamAddDLens : {c : Cat} -> IndCat AddDLens
  54 | FamAddDLens = composeFunctors AddBase (FamIndCat {c=c})
  55 | 
  56 | -- need to check everything from here onwards
  57 | --------------------------------------------------------------------------------
  58 | -- Dependent Types in Poly (Category of Containers & Dependent Lenses)
  59 | --
  60 | -- Reference: von Glehn, "Polynomials and Models of Type Theory", Section 4.1
  61 | --
  62 | -- Key insight: Poly is NOT locally cartesian closed, but:
  63 | --   1. Dependent sums (Σ-types) always exist
  64 | --   2. Dependent products (Π-types) exist only along cartesian morphisms
  65 | --------------------------------------------------------------------------------
  66 | 
  67 | --------------------------------------------------------------------------------
  68 | -- IN TYPE
  69 | --
  70 | -- A type family over `a` is: `a -> Type`
  71 | -- The dependent pair is:     `(x : a ** fam x)`
  72 | -- The dependent function is: `(x : a) -> fam x`
  73 | --------------------------------------------------------------------------------
  74 | 
  75 | namespace Type
  76 |   public export
  77 |   IndexedType : Type -> Type
  78 |   IndexedType a = a -> Type
  79 |   
  80 |   public export
  81 |   TypeDPair : {a : Type} -> IndexedType a -> Type
  82 |   TypeDPair fam = (x : a ** fam x)
  83 | 
  84 |   public export
  85 |   TypeDFun : {a : Type} -> IndexedType a -> Type
  86 |   TypeDFun fam = (x : a) -> fam x
  87 | 
  88 | namespace Cont
  89 |   public export
  90 |   IndexedCont : Cont -> Type
  91 |   IndexedCont c = c.Shp -> Cont
  92 |   
  93 |   public export
  94 |   ContDPair : {a : Cont} -> IndexedCont a -> Cont
  95 |   ContDPair a' = ((x ** t) : DPair a.Shp (Shp . a')) !> (a' x).Pos t
  96 | 
  97 |   public export
  98 |   ContProbDPair : {a : Cont} -> IndexedCont a -> Cont
  99 |   ContProbDPair a' = (((x, d) ** t) : DPair (a.Shp, Double) (Shp . a' . fst)) !>
 100 |     (a' x).Pos t
 101 | 
 102 | namespace AddCont
 103 |   public export
 104 |   IndexedAddCont : AddCont -> Type
 105 |   IndexedAddCont c = c.Shp -> AddCont
 106 | 
 107 |   public export
 108 |   AddContDPair : {a : AddCont} -> IndexedAddCont a -> AddCont
 109 |   AddContDPair a' = MkAddCont
 110 |     (((x ** t) : DPair a.Shp ((.Shp) . a')) !> (a' x).Pos t)
 111 |     {mon=(?MonDPairAddCont)}
 112 | 
 113 | 
 114 |   public export
 115 |   AddContDFunFinite : {n : Nat} -> (Fin n -> AddCont) -> AddCont
 116 |   AddContDFunFinite {n = 0} i = Scalar
 117 |   AddContDFunFinite {n = (S k)} i = i 0 >< AddContDFunFinite (i . FS)
 118 | 
 119 |   public export
 120 |   indexShp : {n : Nat} -> {i : Fin n -> AddCont} ->
 121 |     (j : Fin n) ->
 122 |     (AddContDFunFinite i).Shp -> (i j).Shp
 123 |   indexShp {n = (S k)} FZ (s, _) = s
 124 |   indexShp {n = (S k)} {i} (FS y) (_, ss) = indexShp {i=i . FS} y ss
 125 | 
 126 |   public export
 127 |   AddContDFunction : {a : AddCont} -> IndexedAddCont a -> AddCont
 128 |   AddContDFunction a' = MkAddCont 
 129 |     ((s : (x : a.Shp) -> (a' x).Shp) !> ((x : a.Shp) -> (a' x).Pos (s x)))
 130 |     {mon=(?MonDFunctionAddCont)}
 131 |     --{mon=(MkI @{\s => MkComMonoid
 132 |     --  (\l, r => \x => (a' x).Plus (s x) (l x) (r x))
 133 |     --  (\x => (a' x).Zero (s x))})}
 134 | 
 135 | -- public export
 136 | -- ContDPair : (c : Cont) -> IndexedCont c -> Cont
 137 | -- ContDPair c fam = 
 138 | --   (st : (s : c.Shp ** (fam s).Shp)) !> 
 139 | --   Either (c.Pos (fst st)) ((fam (fst st)).Pos (snd st))
 140 | 
 141 | -- Simpler version: just the family positions (no base positions)
 142 | -- This corresponds to the "total space" of a display map
 143 | public export
 144 | ContDPairSimple : (c : Cont) -> IndexedCont c -> Cont
 145 | ContDPairSimple c fam = 
 146 |   (st : (s : c.Shp ** (fam s).Shp)) !> 
 147 |   (fam (fst st)).Pos (snd st)
 148 | 
 149 | --------------------------------------------------------------------------------
 150 | -- DEPENDENT PRODUCT in Poly (Π-types) — MORE SUBTLE
 151 | --
 152 | -- Π-types do NOT always exist in Poly. When they do exist:
 153 | --   - Shapes: Π(s : S). (fam s).Shp     -- sections of the family
 154 | --   - Positions: Σ(s : S). Σ(p : P s). (fam s).Pos (f s)
 155 | --
 156 | -- This only type-checks when S is "small enough" that we can form Π over it.
 157 | --------------------------------------------------------------------------------
 158 | 
 159 | public export
 160 | ContDFun : (c : Cont) -> IndexedCont c -> Cont
 161 | ContDFun c fam = 
 162 |   (f : ((s : c.Shp) -> (fam s).Shp)) !> 
 163 |   (s : c.Shp ** (p : c.Pos s ** (fam s).Pos (f s)))
 164 | 
 165 | --------------------------------------------------------------------------------
 166 | -- EXAMPLES
 167 | --------------------------------------------------------------------------------
 168 | 
 169 | -- Constant family: assigns the same container to every shape
 170 | public export
 171 | constFam : {c : Cont} -> Cont -> IndexedCont c
 172 | constFam d = \_ => d
 173 | 
 174 | -- Trivial family: assigns the unit container (one shape, no positions) to every shape
 175 | public export
 176 | trivialFam : {c : Cont} -> IndexedCont c
 177 | trivialFam = \_ => ((_ : ()) !> Void)
 178 | 
 179 | -- Family that assigns Bool shapes with no positions
 180 | public export
 181 | boolFam : {c : Cont} -> IndexedCont c
 182 | boolFam = \_ => ((_ : Bool) !> Void)
 183 | 
 184 | --------------------------------------------------------------------------------
 185 | -- COMPARISON WITH CHARTS/LENSES
 186 | --
 187 | -- A chart `c =&> d` is a MORPHISM in Poly, involving both shapes AND positions.
 188 | -- A family `c.Shp -> Cont` is just a FUNCTION on shapes.
 189 | --
 190 | -- Charts give richer structure (relating positions), but families are simpler
 191 | -- and sufficient for forming dependent sums and products.
 192 | --
 193 | -- You CAN extract a family from certain charts:
 194 | --------------------------------------------------------------------------------
 195 | 
 196 | -- The "universe" container: shapes are types, positions are their elements  
 197 | public export
 198 | ContUniverse : Cont
 199 | ContUniverse = (t : Type) !> t
 200 | 
 201 | -- From a chart to Universe, extract just the shape-level data as a family
 202 | -- (This loses the position-level information from the chart!)
 203 | public export
 204 | famFromChart : (c : Cont) -> (f : c =&> ContUniverse) -> IndexedCont c
 205 | famFromChart c f = \s => ((_ : f.fwd s) !> Void)
 206 |   -- We get family shapes from f.fwd, but lose the f.bwd data
 207 |   -- The chart's f.bwd : (s : c.Shp) -> c.Pos s -> f.fwd s 
 208 |   -- doesn't fit into ContFam's structure
 209 | 
 210 | --------------------------------------------------------------------------------
 211 | -- WHY Poly ISN'T LOCALLY CARTESIAN CLOSED
 212 | --
 213 | -- In a locally cartesian closed category, for any morphism f : A -> B,
 214 | -- the pullback functor f* : C/B -> C/A has a right adjoint Πf.
 215 | --
 216 | -- In Poly, this fails for general dependent lenses. The right adjoint
 217 | -- only exists for CARTESIAN morphisms (where the backward map is an iso).
 218 | --
 219 | -- Reference: von Glehn thesis, Section 4.3
 220 | --------------------------------------------------------------------------------
 221 |