From 0e90403fc695b70830c9c8304b6c4adb3f3b2828 Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Tue, 9 Jun 2015 14:46:57 +0200
Subject: [PATCH] Equivalences instead of isos (wip)

---
 Eval.hs        | 81 +++++++++++++++++++++++++++++++++-----------------
 Resolver.hs    |  8 ++---
 TypeChecker.hs | 69 +++++++++++++++++++++++++++++++-----------
 3 files changed, 108 insertions(+), 50 deletions(-)

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