Equivalences instead of isos (wip)

diff --git a/Eval.hs b/Eval.hs
index 4f28dbfdc637890d134e8749aad82b5f9d24a9bd..2c02e03d4f35841424d2a3ccd3767ac8d982f233 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -361,14 +361,11 @@ comp i a u ts = case a of
   VU -> glue u (Map.map (eqToIso . VPath i) ts)
   VGlue b hisos -> compGlue i b hisos u ts
   Ter (Sum _ _ nass) env -> case u of
-    VCon n us -> case lookupLabel n nass of
-      Just as ->
-        if all isCon (elems ts)
-           then let tsus = transposeSystemAndList (Map.map unCon ts) us
-                in VCon n $ comps i as env tsus
-           else VComp (VPath i a) u (Map.map (VPath i) ts)
+    VCon n us | all isCon (elems ts) -> case lookupLabel n nass of
+      Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us
+                 in VCon n $ comps i as env tsus
       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
-    _ -> error $ "comp ter sum" ++ show u
+    _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
   Ter (HSum _ _ nass) env -> compHIT i a u ts
   _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
 
@@ -425,6 +422,7 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One
 -------------------------------------------------------------------------------
 -- | Glue
 --
+-- OLD:
 -- An hiso for a type b is a five-tuple: (a,f,g,r,s)   where
 --  a : U
 --  f : a -> b
@@ -432,6 +430,13 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One
 --  s : forall (y : b), f (g y) = y
 --  t : forall (x : a), g (f x) = x
 
+-- An equivalence for a type b is a four-tuple (a,f,s,t) where
+-- a : U
+-- f : a -> b
+-- s : (y : b) -> fiber a b f y
+-- t : (y : b) (w : fiber a b f y) -> s y = w
+-- with fiber a b f y = (x : a) * (f x = y)
+
 hisoDom :: Val -> Val
 hisoDom (VPair a _) = a
 hisoDom x           = error $ "HisoDom: Not an hiso: " ++ show x
@@ -544,28 +549,48 @@ pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us'
 -- Grad Lemma, takes an iso f, a system us and a value v, s.t. f us =
 -- border v. Outputs (u,p) s.t. border u = us and a path p between v
 -- and f u.
+-- gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
+-- gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v =
+--   (u, VPath i theta'')
+--   where i:j:_   = freshs (b,hiso,us,v)
+--         us'     = mapWithKey (\alpha uAlpha ->
+--                                    app (t `face` alpha) uAlpha @@ i) us
+--         gv      = app g v
+--         theta   = fill i a gv us'
+--         u       = comp i a gv us'  -- Same as "theta `face` (i ~> 1)"
+--         ws      = insertSystem (i ~> 0) gv $
+--                   insertSystem (i ~> 1) (app t u @@ j) $
+--                   mapWithKey
+--                     (\alpha uAlpha ->
+--                       app (t `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
+--         theta'  = compNeg j a theta ws
+--         xs      = insertSystem (i ~> 0) (app s v @@ j) $
+--                   insertSystem (i ~> 1) (app s (app f u) @@ j) $
+--                   mapWithKey
+--                     (\alpha uAlpha ->
+--                       app (s `face` alpha) (app (f `face` alpha) uAlpha) @@ j) us
+--         theta'' = comp j b (app f theta') xs
+
+-- Grad Lemma, takes an equivalence f, an L-system us and a value v,
+-- s.t. f us = border v. Outputs (u,p) s.t. border u = us and an
+-- L-path p between v and f u.
 gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
-gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v =
-  (u, VPath i theta'')
-  where i:j:_   = freshs (b,hiso,us,v)
-        us'     = mapWithKey (\alpha uAlpha ->
-                                   app (t `face` alpha) uAlpha @@ i) us
-        gv      = app g v
-        theta   = fill i a gv us'
-        u       = comp i a gv us'  -- Same as "theta `face` (i ~> 1)"
-        ws      = insertSystem (i ~> 0) gv $
-                  insertSystem (i ~> 1) (app t u @@ j) $
-                  mapWithKey
-                    (\alpha uAlpha ->
-                      app (t `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
-        theta'  = compNeg j a theta ws
-        xs      = insertSystem (i ~> 0) (app s v @@ j) $
-                  insertSystem (i ~> 1) (app s (app f u) @@ j) $
-                  mapWithKey
-                    (\alpha uAlpha ->
-                      app (s `face` alpha) (app (f `face` alpha) uAlpha) @@ j) us
-        theta'' = comp j b (app f theta') xs
-
+gradLemma b equiv@(VPair a (VPair f (VPair s t))) us v =
+  (u,VPath j $ tau `sym` j)
+  where i:j:_ = freshs (b,equiv,us,v)
+        g y = fstVal (app s y) -- g : b -> a
+        eta y = sndVal (app s y) -- eta b @ i : f (g b) --> b
+        us' = mapWithKey
+              (\alpha uAlpha ->
+                let fuAlpha = app (f `face` alpha) uAlpha
+                in app (app (t `face` alpha) fuAlpha)
+                       (VPair uAlpha (constPath fuAlpha))) us
+        theta = fill i a (g v) (Map.map (fstVal . (@@ i)) us')
+        u = theta `face` (i ~> 1)
+        vs = insertsSystem
+               [(j ~> 0, app f theta),(j ~> 1, v)]
+               (Map.map ((@@ j) . sndVal . (@@ i)) us')
+        tau = comp i b (eta v @@ j) vs
 
 -------------------------------------------------------------------------------
 -- | Conversion

diff --git a/Resolver.hs b/Resolver.hs
index c6937374d7873c24831d5da9bc12de93e29c8ba7..7d6e8637169bdae43ad7e6c49231b452b525bdcd 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -207,10 +207,10 @@ resolveExp e = case e of
   Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Glue u ts   -> do
     rs <- resolveSystem ts
-    let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True
-        isIso _ = False
-    unless (all isIso $ Map.elems rs)
-      (throwError $ "Not a system of isomorphisms: " ++ show rs)
+    let isEquiv (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _))) = True
+        isEquiv _ = False
+    unless (all isEquiv $ Map.elems rs)
+      (throwError $ "Not a system of equivalences: " ++ show rs)
     CTT.Glue <$> resolveExp u <*> pure rs
   -- GlueElem u ts      -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
   -- GlueLine phi psi u ->

diff --git a/TypeChecker.hs b/TypeChecker.hs
index aa5331670640d802798eb3764ee6901ad9152016..857f04bfa56972cf53e08434339dd33207de0292 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -112,17 +112,34 @@ mkVars ns ((x,a):xas) nu =
   let w@(VVar n _) = mkVarNice ns x (eval nu a)\r
   in (x,w) : mkVars (n:ns) xas (upd (x,w) nu)\r
 \r
--- Construct a fuction "(_ : va) -> vb"\r
+-- Construct "(_ : va) -> vb"\r
 mkFun :: Val -> Val -> Val\r
 mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))\r
   where rho = upd ("b",vb) (upd ("a",va) empty)\r
 \r
--- Construct "(x : b) -> IdP (<_> b) (f (g x)) x"\r
-mkSection :: Val -> Val -> Val -> Val\r
-mkSection vb vf vg =\r
-  VPi vb (eval rho (Lam "x" b (IdP (Path (Name "_") b) (App f (App g x)) x)))\r
-  where [b,x,f,g] = map Var ["b","x","f","g"]\r
-        rho = upd ("g",vg) (upd ("f",vf) (upd ("b",vb) empty))\r
+-- -- Construct "(x : b) -> IdP (<_> b) (f (g x)) x"\r
+-- mkSection :: Val -> Val -> Val -> Val\r
+-- mkSection vb vf vg =\r
+--   VPi vb (eval rho (Lam "x" b (IdP (Path (Name "_") b) (App f (App g x)) x)))\r
+--   where [b,x,f,g] = map Var ["b","x","f","g"]\r
+--         rho = upd ("g",vg) (upd ("f",vf) (upd ("b",vb) empty))\r
+\r
+-- Construct "(y : b) -> (x : va) * Id vb (vf x) y"\r
+mkFiberCenter :: Val -> Val -> Val -> Val\r
+mkFiberCenter va vb vf =\r
+  eval rho $ Pi (Lam "y" b $\r
+    Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y))\r
+  where [a,b,f,x,y] = map Var ["a","b","f","x","y"]\r
+        rho = upds (zip ["a","b","f"] [va,vb,vf]) empty\r
+\r
+-- Construct "(y : vb) (w : fiber va vb vf y) -> vs y = w\r
+mkFiberIsCenter :: Val -> Val -> Val -> Val -> Val\r
+mkFiberIsCenter va vb vf vs =\r
+  eval rho $ Pi (Lam "y" b $\r
+    Pi (Lam "w" fib $ IdP (Path (Name "_") fib) (App s y) w))\r
+  where [a,b,f,x,y,s,w] = map Var ["a","b","f","x","y","s","w"]\r
+        rho = upds (zip ["a","b","f","s"] [va,vb,vf,vs]) empty\r
+        fib = Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y)\r
 \r
 -- Test if two values are convertible\r
 (===) :: Convertible a => a -> a -> Typing Bool\r
@@ -296,22 +313,38 @@ checkGlue va ts = do
   rho <- asks env\r
   checkCompSystem (evalSystem rho ts)\r
 \r
--- An iso for a type b is a five-tuple: (a,f,g,r,s)   where\r
---  a : U\r
---  f : a -> b\r
---  g : b -> a\r
---  s : forall (y : b), f (g y) = y\r
---  t : forall (x : a), g (f x) = x\r
+-- -- An iso for a type b is a five-tuple: (a,f,g,r,s)   where\r
+-- --  a : U\r
+-- --  f : a -> b\r
+-- --  g : b -> a\r
+-- --  s : forall (y : b), f (g y) = y\r
+-- --  t : forall (x : a), g (f x) = x\r
+-- checkIso :: Val -> Ter -> Typing ()\r
+-- checkIso vb (Pair a (Pair f (Pair g (Pair s t)))) = do\r
+--   check VU a\r
+--   va <- evalTyping a\r
+--   check (mkFun va vb) f\r
+--   check (mkFun vb va) g\r
+--   vf <- evalTyping f\r
+--   vg <- evalTyping g\r
+--   check (mkSection vb vf vg) s\r
+--   check (mkSection va vg vf) t\r
+\r
+-- An equivalence for a type b is a four-tuple (a,f,s,t) where\r
+-- a : U\r
+-- f : a -> b\r
+-- s : (y : b) -> fiber a b f y\r
+-- t : (y : b) (w : fiber a b f y) -> s y = w\r
+-- with fiber a b f y = (x : a) * (f x = y)\r
 checkIso :: Val -> Ter -> Typing ()\r
-checkIso vb (Pair a (Pair f (Pair g (Pair s t)))) = do\r
+checkIso vb (Pair a (Pair f (Pair s t))) = do\r
   check VU a\r
   va <- evalTyping a\r
   check (mkFun va vb) f\r
-  check (mkFun vb va) g\r
   vf <- evalTyping f\r
-  vg <- evalTyping g\r
-  check (mkSection vb vf vg) s\r
-  check (mkSection va vg vf) t\r
+  check (mkFiberCenter va vb vf) s\r
+  vs <- evalTyping s\r
+  check (mkFiberIsCenter va vb vf vs) t\r
 \r
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r