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 | -- public export
 88 | -- ContDPair : (c : Cont) -> IndexedCont c -> Cont
 89 | -- ContDPair c fam = 
 90 | --   (st : (s : c.Shp ** (fam s).Shp)) !> 
 91 | --   Either (c.Pos (fst st)) ((fam (fst st)).Pos (snd st))
 92 |
 93 | -- Simpler version: just the family positions (no base positions)
 94 | -- This corresponds to the "total space" of a display map
 95 | public export
 96 | ContDPairSimple : (c : Cont) -> IndexedCont c -> Cont
 97 | ContDPairSimple c fam = 
 98 |   (st : (s : c.Shp ** (fam s).Shp)) !> 
 99 |   (fam (fst st)).Pos (snd st)
100 |
101 | --------------------------------------------------------------------------------
102 | -- DEPENDENT PRODUCT in Poly (Π-types) — MORE SUBTLE
103 | --
104 | -- Π-types do NOT always exist in Poly. When they do exist:
105 | --   - Shapes: Π(s : S). (fam s).Shp     -- sections of the family
106 | --   - Positions: Σ(s : S). Σ(p : P s). (fam s).Pos (f s)
107 | --
108 | -- This only type-checks when S is "small enough" that we can form Π over it.
109 | --------------------------------------------------------------------------------
110 |
111 | public export
112 | ContDFun : (c : Cont) -> IndexedCont c -> Cont
113 | ContDFun c fam = 
114 |   (f : ((s : c.Shp) -> (fam s).Shp)) !> 
115 |   (s : c.Shp ** (p : c.Pos s ** (fam s).Pos (f s)))
116 |
117 | --------------------------------------------------------------------------------
118 | -- EXAMPLES
119 | --------------------------------------------------------------------------------
120 |
121 | -- Constant family: assigns the same container to every shape
122 | public export
123 | constFam : {c : Cont} -> Cont -> IndexedCont c
124 | constFam d = \_ => d
125 |
126 | -- Trivial family: assigns the unit container (one shape, no positions) to every shape
127 | public export
128 | trivialFam : {c : Cont} -> IndexedCont c
129 | trivialFam = \_ => ((_ : ()) !> Void)
130 |
131 | -- Family that assigns Bool shapes with no positions
132 | public export
133 | boolFam : {c : Cont} -> IndexedCont c
134 | boolFam = \_ => ((_ : Bool) !> Void)