Don't require equivalences to be eta-expanded

diff --git a/Eval.hs b/Eval.hs
index 7103af6fbd9165705d8fbc19ca0a0b3e7a8bdf73..21bc5551c26dbd3342fa47f9687df28202e2561e 100644 (file)
--- 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 7d6e8637169bdae43ad7e6c49231b452b525bdcd..96ddc4d3b8336436fb6acb8f732128d1409e8f1f 100644 (file)
--- 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 13d0ba796826892732e9097d514e3264d1e2ce10..c1b33e41c8cf8d7505af9ea09d019e1c22eafa43 100644 (file)
--- 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)\r
   in (x,w) : mkVars (n:ns) xas (upd (x,w) nu)\r
 \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
-\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
 u === v = conv <$> asks names <*> pure u <*> pure v\r
@@ -319,15 +290,18 @@ checkGlue va ts = do
 -- 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
+mkEquiv :: Val -> Val\r
+mkEquiv vb = eval rho $\r
+  Sigma $ Lam "a" U $\r
+  Sigma $ Lam "f" (Pi (Lam "_" a b)) $\r
+  Sigma $ Lam "s" (Pi (Lam "y" b $ fib)) $\r
+    Pi (Lam "y" b $ 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 = upd ("b",vb) empty\r
+        fib = Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y)\r
+\r
 checkEquiv :: Val -> Ter -> Typing ()\r
-checkEquiv vb (Pair a (Pair f (Pair s t))) = do\r
-  check VU a\r
-  va <- evalTyping a\r
-  check (mkFun va vb) f\r
-  vf <- evalTyping f\r
-  check (mkFiberCenter va vb vf) s\r
-  vs <- evalTyping s\r
-  check (mkFiberIsCenter va vb vf vs) t\r
+checkEquiv vb equiv = check (mkEquiv vb) equiv\r
 \r
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r
@@ -390,7 +364,9 @@ checkPathSystem t0 va ps = do
       rhoAlpha <- asks env\r
       (a0,a1)  <- checkPath (va `face` alpha) pAlpha\r
       unlessM (a0 === eval rhoAlpha t0) $\r
-        throwError $ "Incompatible system " ++ showSystem ps ++ " with " ++ show t0\r
+        throwError $ "Incompatible system " ++ showSystem ps ++\r
+                     ", component\n " ++ show pAlpha ++\r
+                     "\nincompatible  with\n " ++ show t0\r
       return a1) ps\r
   checkCompSystem (evalSystem rho ps)\r
   return v\r