From: Anders Mörtberg 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 = - 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 = + glue B [ (i = 0) -> (A,f,g,s,t) + , (i = 1) -> (B,idfun B,idfun B,refl B,refl B) ]