From: Simon Huber <hubsim@gmail.com>
Date: Tue, 16 Jun 2015 08:15:22 +0000 (+0200)
Subject: Don't require equivalences to be eta-expanded
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=86d23727c88aa18870a311f44460c8ab0fdc6428;p=cubicaltt.git

Don't require equivalences to be eta-expanded
---

diff --git a/Eval.hs b/Eval.hs
index 7103af6..21bc555 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -429,13 +429,10 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One
 -- with fiber a b f y = (x : a) * (f x = y)
 
 equivDom :: Val -> Val
-equivDom (VPair a _) = a
-equivDom x           = error $ "equivDom: Not an equivalence: " ++ show x
+equivDom = fstVal
 
 equivFun :: Val -> Val
-equivFun (VPair _ (VPair f _)) = f
-equivFun x                     =
-  error $ "equivFun: Not an equivalence: " ++ show x
+equivFun = sndVal . fstVal
 
 -- TODO: adapt to equivs
 -- Every path in the universe induces an hiso
@@ -465,19 +462,11 @@ equivFun x                     =
 --                         ,(j ~> 1, inv (edown x))]
 --         t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv
 
--- 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)
-
-
 -- Every path in the universe induces an equivalence
 eqToEquiv :: Val -> Val
 eqToEquiv e = VPair e1 (VPair f (VPair s t))
   where e1 = e @@ One
-        (i,j,k,x,y,w,ev) = (Name "i",Name "j",Name "k",Var "x",Var "y",Var "w",Var "E")
+        (i,j,x,y,w,ev) = (Name "i",Name "j",Var "x",Var "y",Var "w",Var "E")
         inv t = Path i $ AppFormula t (NegAtom i)
         evinv = inv ev
         (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a)
diff --git a/Resolver.hs b/Resolver.hs
index 7d6e863..96ddc4d 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -205,13 +205,7 @@ resolveExp e = case e of
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
   Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
-  Glue u ts   -> do
-    rs <- resolveSystem ts
-    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
+  Glue u ts   -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
   -- GlueElem u ts      -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
   -- GlueLine phi psi u ->
   --   CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi
diff --git a/TypeChecker.hs b/TypeChecker.hs
index 13d0ba7..c1b33e4 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -112,35 +112,6 @@ 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 "(_ : 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 "(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
 u === v = conv <$> asks names <*> pure u <*> pure v
@@ -319,15 +290,18 @@ checkGlue va ts = do
 -- 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)
+mkEquiv :: Val -> Val
+mkEquiv vb = eval rho $
+  Sigma $ Lam "a" U $
+  Sigma $ Lam "f" (Pi (Lam "_" a b)) $
+  Sigma $ Lam "s" (Pi (Lam "y" b $ fib)) $
+    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 = upd ("b",vb) empty
+        fib = Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y)
+
 checkEquiv :: Val -> Ter -> Typing ()
-checkEquiv vb (Pair a (Pair f (Pair s t))) = do
-  check VU a
-  va <- evalTyping a
-  check (mkFun va vb) f
-  vf <- evalTyping f
-  check (mkFiberCenter va vb vf) s
-  vs <- evalTyping s
-  check (mkFiberIsCenter va vb vf vs) t
+checkEquiv vb equiv = check (mkEquiv vb) equiv
 
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do
@@ -390,7 +364,9 @@ checkPathSystem t0 va ps = do
       rhoAlpha <- asks env
       (a0,a1)  <- checkPath (va `face` alpha) pAlpha
       unlessM (a0 === eval rhoAlpha t0) $
-        throwError $ "Incompatible system " ++ showSystem ps ++ " with " ++ show t0
+        throwError $ "Incompatible system " ++ showSystem ps ++
+                     ", component\n " ++ show pAlpha ++
+                     "\nincompatible  with\n " ++ show t0
       return a1) ps
   checkCompSystem (evalSystem rho ps)
   return v