From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 30 Jun 2015 19:27:00 +0000 (+0200)
Subject: Fix typo in typechecker and redefine isoId using glue
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7da5c1217fcb5d3754a7c51d5f5461438fad4ec7;p=cubicaltt.git

Fix typo in typechecker and redefine isoId using glue
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 0d0e62d..c0af283 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -286,7 +286,7 @@ mkIso :: Val -> Val
 mkIso vb = eval rho $
   Sigma $ Lam "a" U $
   Sigma $ Lam "f" (Pi (Lam "_" a b)) $
-  Sigma $ Lam "b" (Pi (Lam "_" b a)) $
+  Sigma $ Lam "g" (Pi (Lam "_" b a)) $
   Sigma $ Lam "s" (Pi (Lam "y" b $ IdP (Path (Name "_") b) (App f (App g y)) y)) $
     Pi (Lam "x" a $ IdP (Path (Name "_") a) (App g (App f x)) x)
   where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"]
diff --git a/examples/gradLemma.ctt b/examples/gradLemma.ctt
index c1d5367..41ab643 100644
--- 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 3af7ae7..da8bf9b 100644
--- 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) ]