Fix typo in typechecker and redefine isoId using glue

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 0d0e62dc98bd4fe65b1f6c2ed748befb1ce7f10d..c0af28389250f62fa59a43a309741599fafa4fa2 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -286,7 +286,7 @@ mkIso :: Val -> Val
 mkIso vb = eval rho $\r
   Sigma $ Lam "a" U $\r
   Sigma $ Lam "f" (Pi (Lam "_" a b)) $\r
-  Sigma $ Lam "b" (Pi (Lam "_" b a)) $\r
+  Sigma $ Lam "g" (Pi (Lam "_" b a)) $\r
   Sigma $ Lam "s" (Pi (Lam "y" b $ IdP (Path (Name "_") b) (App f (App g y)) y)) $\r
     Pi (Lam "x" a $ IdP (Path (Name "_") a) (App g (App f x)) x)\r
   where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"]\r

diff --git a/examples/gradLemma.ctt b/examples/gradLemma.ctt
index c1d536762388489ba4ed1edc1bd913db4a7362ed..41ab64385d94b8a490ec4828636505c9fa95537e 100644 (file)
--- a/examples/gradLemma.ctt
+++ b/examples/gradLemma.ctt
@@ -62,13 +62,6 @@ gradLemma (A B : U) (f : A -> B) (g : B -> A)
     fIsCenter (y : B) (w : fiber A B f y) : Id (fiber A B f y) (fCenter y) w =
       lemIso A B f g s t y (fCenter y).1 w.1 (fCenter y).2 w.2
 
--- Using gradLemma we get that any isomorphism gives a line in the universe
-isoId (A B : U) (f : A -> B) (g : B -> A)
-      (s : (y : B) -> Id B (f (g y)) y)
-      (t : (x : A) -> Id A (g (f x)) x) : Id U A B =
-      <i> glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
-                 , (i = 1) -> (B,transDelta B) ]
-
 
 -- OLD CODE:
 -- lemIso with equalities on other direction:

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 3af7ae76fc7e67b47c47d980068c5512c6e1c34c..da8bf9b775aa6ba2d735aebff31bc0d16c4df020 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -236,3 +236,10 @@ injective (A B : U) (f : A -> B) : U =
   (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1
 
 and (A B : U) : U = (_ : A) * B
+
+
+isoId (A B : U) (f : A -> B) (g : B -> A)
+      (s : (y : B) -> Id B (f (g y)) y)
+      (t : (x : A) -> Id A (g (f x)) x) : Id U A B =
+      <i> glue B [ (i = 0) -> (A,f,g,s,t)
+                 , (i = 1) -> (B,idfun B,idfun B,refl B,refl B) ]