rename gradLemma to isoToEquiv

diff --git a/Eval.hs b/Eval.hs
index e013605f3a2bac0846eb581b6c8be31d638a15ee..25f09c555a0e9411c58860f4a5f682bf8c0c1711 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -762,7 +762,7 @@ lemEq eq b aps = (a,VPLam i (compNeg j (eq @@ j) p1 thetas'))
 --         -- for gamma in es'', (i1) gamma is in es, so wsi1 gamma
 --         -- is in the domain of isoGamma
 --         uls'' = mapWithKey (\gamma eGamma ->
---                   gradLemmaU (bi1 `face` gamma) eGamma
+--                   isoToEquivU (bi1 `face` gamma) eGamma
 --                     ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma))
 --                     (vi1' `face` gamma))
 --                   es''
@@ -777,11 +777,11 @@ lemEq eq b aps = (a,VPLam i (compNeg j (eq @@ j) p1 thetas'))
 --                      else fst (uls'' ! gamma))
 --                   esI1
 
--- Grad Lemma, takes a line eq in U, a system us and a value v, s.t. f us =
+-- IsoToEquiv, takes a line eq in U, a system us and a value v, s.t. f us =
 -- border v. Outputs (u,p) s.t. border u = us and a path p between v
 -- and f u, where f is transNegLine eq
--- gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val)
--- gradLemmaU b eq us v = (u, VPLam i theta)
+-- isoToEquivU :: Val -> Val -> System Val -> Val -> (Val, Val)
+-- isoToEquivU b eq us v = (u, VPLam i theta)
 --   where i:j:_   = freshs (b,eq,us,v)
 --         ej      = eq @@ j
 --         a       = eq @@ One
@@ -794,8 +794,8 @@ lemEq eq b aps = (a,VPLam i (compNeg j (eq @@ j) p1 thetas'))
 --         theta   = compNeg j ej u xs
 
 -- Old version:
--- gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val)
--- gradLemmaU b eq us v = (u, VPLam i theta'')
+-- isoToEquivU :: Val -> Val -> System Val -> Val -> (Val, Val)
+-- isoToEquivU b eq us v = (u, VPLam i theta'')
 --   where i:j:_   = freshs (b,eq,us,v)
 --         a       = eq @@ One
 --         g       = transLine

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 89b365d96dd591447c950b13693ce06048ca113a..0759a624cd6a51b4f30ff269d8b61ad1094228d3 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -82,7 +82,7 @@ negBoolK : (b : bool) -> Path bool (negBool (negBool b)) b = split
 
 -- negBool is hence and equivalence:
 negBoolEquiv : equiv bool bool =
-  (negBool,gradLemma bool bool negBool negBool negBoolK negBoolK)
+  (negBool,isoToEquiv bool bool negBool negBool negBoolK negBoolK)
 
 -- This defines a non-trivial equality between bool and bool:
 negBoolEq : Path U bool bool =
@@ -168,7 +168,7 @@ q : Path U F2 F2 = <i> p @ (i /\ - i)
 
 -- A small test of univalence using boolean negation
 isEquivNegBool : isEquiv bool bool negBool =
- gradLemma bool bool negBool negBool negBoolK negBoolK
+ isoToEquiv bool bool negBool negBool negBoolK negBoolK
 
 eqBool : Path U bool bool =
  trans (equiv bool bool) (Path U bool bool)

diff --git a/examples/category.ctt b/examples/category.ctt
index 71ff7f3d3bfcbd55b68e005653b8508b68109017..34dfc87cca12682385e83ceb4d1ed56cb7e6e2c7 100644 (file)
--- a/examples/category.ctt
+++ b/examples/category.ctt
@@ -47,7 +47,7 @@ isContrProp (A : U) (p : isContr A) (x y : A) : Path A x y = compPath A x p.1 y
 opaque isContrProp
 
 equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =
-  (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
+  (F, isoToEquiv A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
 opaque equivProp
 
 idProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : Path U A B
@@ -155,7 +155,7 @@ invIso (C : precategory) (A B : cA C) (f : iso C A B) : iso C B A = (f.2.1, f.1,
 idIso (C : precategory) (A : cA C) : iso C A A = (cPath C A, cPath C A, cPathL C A A (cPath C A), cPathL C A A (cPath C A))
 
 invIsoEquiv (C : precategory) (A B : cA C) : isEquiv (iso C A B) (iso C B A) (invIso C A B)
-  = gradLemma (iso C A B) (iso C B A) (invIso C A B) (invIso C B A) (\(x : iso C B A) -> <_> x) (\(x : iso C A B) -> <_> x)
+  = isoToEquiv (iso C A B) (iso C B A) (invIso C A B) (invIso C B A) (\(x : iso C B A) -> <_> x) (\(x : iso C A B) -> <_> x)
 
 invIsoEq (C : precategory) (A B : cA C) : Path U (iso C A B) (iso C B A)
   = equivPath (iso C A B) (iso C B A) (invIso C A B) (invIsoEquiv C A B)
@@ -789,7 +789,7 @@ sigEquivLem (A A':U) (B:A->U) (B':A'->U)
             (e:equiv A A')
             (f:(x:A)->equiv (B x) (B' (e.1 x)))
           : equiv (Sigma A B) (Sigma A' B')
-          = (F, gradLemma (Sigma A B) (Sigma A' B') F G FG GF)
+          = (F, isoToEquiv (Sigma A B) (Sigma A' B') F G FG GF)
   where
     F (x:Sigma A B):Sigma A' B' = (e.1 x.1, (f x.1).1 x.2)
     G (x:Sigma A' B'):Sigma A B = ((e.2 x.1).1.1, ((f (e.2 x.1).1.1).2 (transport (<i> B' ((e.2 x.1).1.2 @ i)) x.2)).1.1)
@@ -846,7 +846,7 @@ eCatIso32 (A B : precategory) : Path U (catIso31 A B) (catIso32 A B)
         (sigEquivLem (catIso311 A B e1) (catIso321 A B e1)
          (\(e2 : catIso311 A B e1) -> (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2))
          (\(e2 : catIso321 A B e1) -> (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2))
-          (F, gradLemma (catIso311 A B e1) (catIso321 A B e1)
+          (F, isoToEquiv (catIso311 A B e1) (catIso321 A B e1)
                F (\(e2:catIso321 A B e1)-><i>\(x y:cA A)->(e2 x y)@i)
                (\(e2:catIso321 A B e1)-><_>e2) (\(e2:catIso311 A B e1)-><_>e2))
         (\(e2:catIso311 A B e1)->
@@ -854,12 +854,12 @@ eCatIso32 (A B : precategory) : Path U (catIso31 A B) (catIso32 A B)
          (\(_ : catIso312 A B e1 e2) -> (catIso313 A B e1 e2))
          (\(_ : catIso322 A B e1 (F e2)) -> (catIso323 A B e1 (F e2)))
           (let F2(e:catIso312 A B e1 e2):catIso322 A B e1 (F e2)=\(x:cA A)-><i>(e@i)x in
-           (F2, gradLemma (catIso312 A B e1 e2) (catIso322 A B e1 (F e2))
+           (F2, isoToEquiv (catIso312 A B e1 e2) (catIso322 A B e1 (F e2))
                  F2 (\(e:catIso322 A B e1 (F e2))-><i>\(x:cA A)->(e x)@i)
                  (\(e:catIso322 A B e1 (F e2))-><_>e) (\(e:catIso312 A B e1 e2)-><_>e)))
         (\(_:catIso312 A B e1 e2)->
          (let F3(e:catIso313 A B e1 e2):catIso323 A B e1 (F e2)=\(x y z:cA A)(f:cH A x y)(g:cH A y z)-><i>(e@i)x y z f g in
-          (F3, gradLemma (catIso313 A B e1 e2) (catIso323 A B e1 (F e2))
+          (F3, isoToEquiv (catIso313 A B e1 e2) (catIso323 A B e1 (F e2))
                 F3 (\(e:catIso323 A B e1 (F e2))-><i>\(x y z:cA A)(f:cH A x y)(g:cH A y z)->(e x y z f g)@i)
                 (\(e:catIso323 A B e1 (F e2))-><_>e) (\(e:catIso313 A B e1 e2)-><_>e))
         )))))) @ i
@@ -882,7 +882,7 @@ catIso2 (A B : precategory) : U = (e1 : equiv (cA A) (cA B))
 
 eCatIso (A B : precategory) : Path U (catIso A B) (catIso2 A B)
   = transEquivToPath (catIso A B) (catIso2 A B)
-    (F, gradLemma (catIso A B) (catIso2 A B) F G (\(e:catIso2 A B)-><_>e) (\(e:catIso A B)-><_>e))
+    (F, isoToEquiv (catIso A B) (catIso2 A B) F G (\(e:catIso2 A B)-><_>e) (\(e:catIso A B)-><_>e))
   where
     F(e:catIso A B):catIso2 A B=((e.1.1, e.2.2),\(x y:cA A)->(e.1.2.1 x y, e.2.1 x y),e.1.2.2.1,e.1.2.2.2)
     G(e:catIso2 A B):catIso A B=((e.1.1,\(x y:cA A)->(e.2.1 x y).1,e.2.2.1,e.2.2.2),\(x y:cA A)->(e.2.1 x y).2,e.1.2)
@@ -900,7 +900,7 @@ catIso23' (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso21' A B e1) :
        (cC B (transport e1 x) (transport e1 y) (transport e1 z) ((e2 x y).1 f) ((e2 y z).1 g))
 
 equivPi (A:U) (B0 B1:A->U) (e:(a:A)->equiv (B0 a) (B1 a)) : equiv ((a:A)->B0 a) ((a:A)->B1 a)
-  = (F, gradLemma ((a:A)->B0 a) ((a:A)->B1 a)
+  = (F, isoToEquiv ((a:A)->B0 a) ((a:A)->B1 a)
                   F (\(g:(a:A)->B1 a)(a:A)->((e a).2 (g a)).1.1)
                   (\(g:(a:A)->B1 a)-><i>\(a:A)->retEq (B0 a) (B1 a) (e a) (g a)@i)
                   (\(f:(a:A)->B0 a)-><i>\(a:A)->secEq (B0 a) (B1 a) (e a) (f a)@i)
@@ -952,7 +952,7 @@ catIsoIsEquiv (A B : precategory) (F : functor A B) (e : catIsIso A B F) : catIs
   = (e.1,\(b:cA B)->((e.2 b).1.1, eqToIso B (F.1 (e.2 b).1.1) b (<i>(e.2 b).1.2@-i)))
 
 invEquiv (A:U) (a b:A) : Path U (Path A a b) (Path A b a)
- = equivPath (Path A a b) (Path A b a) (inv A a b) (gradLemma (Path A a b) (Path A b a) (inv A a b) (inv A b a) (\(x:Path A b a) -> <_> x) (\(x:Path A a b) -> <_> x))
+ = equivPath (Path A a b) (Path A b a) (inv A a b) (isoToEquiv (Path A a b) (Path A b a) (inv A a b) (inv A b a) (\(x:Path A b a) -> <_> x) (\(x:Path A a b) -> <_> x))
 
 catEquivIsIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F : functor A B) (e : catIsEquiv A B F)
   : catIsIso A B F
@@ -963,7 +963,7 @@ catEquivIsIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F
         (transport (<i> isContr ((a:cA A)*lemIsCategory3 B isCB (F.1 a) b@-i)) p))
 
 equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =
-  (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
+  (F, isoToEquiv A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
 
 catIsEquivEqIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F : functor A B)
   : equiv (catIsEquiv A B F) (catIsIso A B F)

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index db4b75bbfed4020d9da89d1b74e1313181fc85ff..d5a80c0bec6e3d4f889b13216fdf93e6e25e333b 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -1,5 +1,5 @@
 -- This file contains the definition of equivalences and various
--- results on these, including the "graduate lemma".
+-- results on these
 module equiv where
 
 import prelude
@@ -98,7 +98,7 @@ idToPath (A B : U) (w : equiv A B)
       (<i>transPathFun A B w@-i)
 
 
--- The grad lemma
+-- The iso to equiv
 
 lemIso (A B : U) (f : A -> B) (g : B -> A)
        (s : (y : B) -> Path B (f (g y)) y)
@@ -149,7 +149,7 @@ lemIso (A B : U) (f : A -> B) (g : B -> A)
                                          , (j = 1) -> s (f (p @ i))
                                          , (j = 0) -> s y ]
 
-gradLemma (A B : U) (f : A -> B) (g : B -> A)
+isoToEquiv (A B : U) (f : A -> B) (g : B -> A)
        (s : (y : B) -> Path B (f (g y)) y)
        (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f =
   \(y:B) -> ((g y,<i>s y@-i),\ (z:fiber A B f y) ->
@@ -158,8 +158,8 @@ gradLemma (A B : U) (f : A -> B) (g : B -> A)
 isoPath (A B : U) (f : A -> B) (g : B -> A)
       (s : (y : B) -> Path B (f (g y)) y)
       (t : (x : A) -> Path A (g (f x)) x) : Path U A B =
-       <i> Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
+       <i> Glue B [ (i = 0) -> (A,f,isoToEquiv A B f g s t)
                   , (i = 1) -> (B,idfun B,idIsEquiv B) ]
 
-idIsEquivGrad (A : U) : isEquiv A A (idfun A) =
-  gradLemma A A (idfun A) (idfun A) (\(a : A) -> <i> a) (\(a : A) -> <i> a)
+idIsEquivIsoToEquiv (A : U) : isEquiv A A (idfun A) =
+  isoToEquiv A A (idfun A) (idfun A) (\(a : A) -> <i> a) (\(a : A) -> <i> a)

diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt
index be8c80f11843cb1765ba8f5446bc9cec37da854b..913e6a9dd5c396962137cce7ef114177dcc63f62 100644 (file)
--- a/examples/idtypes.ctt
+++ b/examples/idtypes.ctt
@@ -74,7 +74,7 @@ idToPathToId (A : U) (a b : A) (p : Id A a b) :
 PathIdPath (A B : U) : Path U (Id U A B) (Path U A B) =
   equivPath (Id U A B) (Path U A B) (idToPath U A B) rem
   where rem : isEquiv (Id U A B) (Path U A B) (idToPath U A B) =
-          gradLemma (Id U A B) (Path U A B) (idToPath U A B) (pathToId U A B)
+          isoToEquiv (Id U A B) (Path U A B) (idToPath U A B) (pathToId U A B)
             (\(p : Path U A B) -> <i> pathToIdToPath U A B p @ - i)
             (\(p : Id U A B) -> <i> idToPathToId U A B p @ - i)
 

diff --git a/examples/subset.ctt b/examples/subset.ctt
index 0df6500f54b45a8632319080b54847bbf9ccc0b4..209029598f2d43cba436ae7e7f64b0225b5f3b70 100644 (file)
--- a/examples/subset.ctt
+++ b/examples/subset.ctt
@@ -113,7 +113,7 @@ subsetIso0 (A : U) (sA : set A) : (s0 : subset0 A sA) ->
     P (X : U) (h: X -> B) : U
       = (p : Path U X B) * (PathP (<i> p @ i -> A) (\ (x : X) -> f' (g (h x))) f)
     q : P B' g'
-      = elimEquiv B P (<i> B, <i> f) B' (g', gradLemma B' B g' g s t)
+      = elimEquiv B P (<i> B, <i> f) B' (g', isoToEquiv B' B g' g s t)
     idB : Path U B' B
       = q.1
     -- Show that sB can be identified with sB'

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index c9faa9e67e63d4ce9d6d9cb6641c09a0571009cc..70133c34376823c8090d7081a18d263ce78bae38 100644 (file)
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -8,7 +8,7 @@ import helix
 \r
 isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isEquiv B C G)\r
   : isEquiv A C (\(x : A) -> G (F x))\r
-  = gradLemma A C (\(x : A) -> G (F x)) (\(x : C) -> (ef (eg x).1.1).1.1)\r
+  = isoToEquiv A C (\(x : A) -> G (F x)) (\(x : C) -> (ef (eg x).1.1).1.1)\r
     (\(x : C) -> compPath C (G (F (ef (eg x).1.1).1.1)) (G (eg x).1.1) x\r
                  (<i> G (retEq A B (F, ef) (eg x).1.1 @ i)) (retEq B C (G, eg) x))\r
     (\(x : A) -> compPath A ((ef (eg (G (F x))).1.1).1.1) (ef (F x)).1.1 x\r
@@ -16,7 +16,7 @@ isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isE
 \r
 isEquivComp' (A B C : U) (F : A -> B) (G : C -> B) (ef : isEquiv A B F) (eg : isEquiv C B G)\r
   : isEquiv A C (\(x : A) -> (eg (F x)).1.1)\r
-  = gradLemma A C (\(x : A) -> (eg (F x)).1.1) (\(x : C) -> (ef (G x)).1.1)\r
+  = isoToEquiv A C (\(x : A) -> (eg (F x)).1.1) (\(x : C) -> (ef (G x)).1.1)\r
     (\(x : C) -> compPath C (eg (F (ef (G x)).1.1)).1.1 (eg (G x)).1.1 x\r
                  (<i> (eg (retEq A B (F, ef) (G x) @ i)).1.1) (secEq C B (G, eg) x))\r
     (\(x : A) -> compPath A ((ef (G (eg (F x)).1.1)).1.1) (ef (F x)).1.1 x\r
@@ -96,7 +96,7 @@ lemPathPSet2 (A B : U) (ASet : set A) (p1 : Path U A B)
     (lemPathPSet A B ASet p1)\r
 \r
 \r
-isEquivPath (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x)\r
+isEquivPath (A : U) : isEquiv A A (\(x : A) -> x) = isoToEquiv A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x)\r
 \r
 lem10 (A B : U) (e : equiv A B) (x y : B) (p : Path A (e.2 x).1.1 (e.2 y).1.1) : Path B x y\r
   = transport\r
@@ -208,7 +208,7 @@ isoPathProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A
   isoPath A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x)\r
 \r
 equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =\r
-  (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))\r
+  (F, isoToEquiv A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))\r
 \r
 isContrProp (A : U) (p : isContr A) (x y : A) : Path A x y = compPath A x p.1 y (<i> p.2 x @ -i) (p.2 y)\r
 \r
@@ -297,7 +297,7 @@ F12 (A B : U) (F : A -> B) (p1 : P1 A B F) (x : A) : isContr ((y : A) * Path B (
     hole  : isContr ((y : A) * Path B (F x) (F y)) = transport (<i> isContr (hole4@i)) (lem2 A x)\r
 \r
 contrEquiv (A B : U) (aC : isContr A) (bC : isContr B) : equiv A B\r
-  = (\(_ : A) -> bC.1, gradLemma A B (\(_ : A) -> bC.1) (\(_ : B) -> aC.1) (\(x : B) -> bC.2 x) (\(x : A) -> aC.2 x))\r
+  = (\(_ : A) -> bC.1, isoToEquiv A B (\(_ : A) -> bC.1) (\(_ : B) -> aC.1) (\(x : B) -> bC.2 x) (\(x : A) -> aC.2 x))\r
 \r
 F21 (A B : U) (F : A -> B) (p2 : P2 A B F) (x y : A) : isEquiv (Path A x y) (Path B (F x) (F y)) (mapOnPath A B F x y) = hole3 y\r
   where\r
@@ -442,7 +442,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Path U (BZSet BA) (BZSet BB)) * PathP (<i> p@i
                    AEquiv BEquiv (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
           hole : Path (Path BZ BA BB) q2 q = <j i> (p@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i)))\r
       hole : equiv ((p : Path U (BZSet BA) (BZSet BB)) * PathP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Path BZ BA BB)\r
-           = (F, gradLemma ((p : Path U (BZSet BA) (BZSet BB)) * PathP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Path BZ BA BB) F G FG GF)\r
+           = (F, isoToEquiv ((p : Path U (BZSet BA) (BZSet BB)) * PathP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Path BZ BA BB) F G FG GF)\r
 \r
 lem2 (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Path A (shift.1 (action A shift a x)) (action A shift a (sucZ x)) = split\r
   inl n -> lem2Aux n\r
@@ -470,7 +470,7 @@ lem2' (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Path A (shift.2 (action A
 \r
 ZBZ : BZ = (Z, (hinhpr Z zeroZ, (ZShift, ZEquiv)))\r
   where\r
-    ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ)\r
+    ZShift : equiv Z Z = (sucZ, isoToEquiv Z Z sucZ predZ sucpredZ predsucZ)\r
     plus : Z -> Z -> Z = action Z ZShift\r
     plusCommZero : (y : Z) -> Path Z (plus zeroZ y) (plus y zeroZ) = split\r
       inl u -> hole u\r
@@ -606,14 +606,14 @@ BZequivBZ' : Path U BZ BZ' = isoPath BZ BZ' F G FG GF
                        where\r
                          SHIFT : isEquiv A.1.1 A.1.1 A.1.2\r
                                = A.2 (isEquiv A.1.1 A.1.1 A.1.2, propIsEquiv A.1.1 A.1.1 A.1.2)\r
-                                 (\(a : Path AA A.1 (Z, sucZ)) -> transport (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ))\r
-                         ZEquiv : (x : Z) -> isEquiv Z Z (action Z (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) x) = BZEquiv ZBZ\r
+                                 (\(a : Path AA A.1 (Z, sucZ)) -> transport (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (isoToEquiv Z Z sucZ predZ sucpredZ predsucZ))\r
+                         ZEquiv : (x : Z) -> isEquiv Z Z (action Z (sucZ, isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) x) = BZEquiv ZBZ\r
                          hole (a : Path AA A.1 (Z, sucZ))\r
-                             : PathP (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ) SHIFT\r
+                             : PathP (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) SHIFT\r
                              = lemPathPProp (isEquiv Z Z sucZ) (isEquiv A.1.1 A.1.1 A.1.2) (propIsEquiv Z Z sucZ)\r
-                               (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ) SHIFT\r
+                               (<i> isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) SHIFT\r
                          ZEquivEq (a : Path AA A.1 (Z, sucZ))\r
-                             : Path U ((x : Z) -> isEquiv Z Z (action Z (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) x))\r
+                             : Path U ((x : Z) -> isEquiv Z Z (action Z (sucZ, isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) x))\r
                                     ((x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x))\r
                              = <i> (x : (a@-i).1) -> isEquiv Z (a@-i).1 (action (a@-i).1 ((a@-i).2, hole a @ i) x)\r
                          EQUIV : (x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x)\r
@@ -711,7 +711,7 @@ multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv)))
     opaque FG\r
     GF (A B : BZ) (x : (Path BZ A B)) : Path (Path BZ A B) (G A B (F A B x)) x = lemCompInv BZ A B B x (loopA B)\r
     opaque GF\r
-    TShift (A B : BZ) : equiv (Path BZ A B) (Path BZ A B) = (F A B, gradLemma (Path BZ A B) (Path BZ A B) (F A B) (G A B) (FG A B) (GF A B))\r
+    TShift (A B : BZ) : equiv (Path BZ A B) (Path BZ A B) = (F A B, isoToEquiv (Path BZ A B) (Path BZ A B) (F A B) (G A B) (FG A B) (GF A B))\r
     hole : (y : Z) -> Path (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) y) (decodeZ ZBZ y) = split\r
       inl u -> hole0 u\r
         where hole0 : (n : nat) -> Path (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) (inl n)) (decodeZ ZBZ (inl n)) = split\r
@@ -735,7 +735,7 @@ multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv)))
                           (decodeLoop (inr n))\r
     transparent decodeZ\r
     TEquiv''' : isEquiv Z (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ))\r
-      = transport (<i> isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (gradLemma Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ))\r
+      = transport (<i> isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (isoToEquiv Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ))\r
     TEquiv'' (b : BZSet B) (x : Path BZ ZBZ B) : isEquiv Z (Path BZ ZBZ B) (action (Path BZ ZBZ B) (TShift ZBZ B) x)\r
       = J BZ ZBZ (\(B : BZ) -> \(x : Path BZ ZBZ B) -> isEquiv Z (Path BZ ZBZ B) (action (Path BZ ZBZ B) (TShift ZBZ B) x))\r
         TEquiv''' B x\r

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index a662d9996d4e5351ef3938b6df476647dd35e753..70bf0265276f4b9690062d6b7a9f4f6adddb04f6 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -167,7 +167,7 @@ univalenceJ (A B : U) : equiv (Path U A B) (equiv A B) =
 -- transEquiv is an equiv
 transEquivIsEquiv (A B : U)
   : isEquiv (Path U A B) (equiv A B) (transEquiv A B)
-  = gradLemma (Path U A B) (equiv A B) (transEquiv A B)
+  = isoToEquiv (Path U A B) (equiv A B) (transEquiv A B)
       (transEquivToPath A B) (idToPath A B) (eqToEq A B)
 
 -- Univalence proved using transEquiv.
@@ -281,7 +281,7 @@ elimIso (B : U) (Q : (A : U) -> (A -> B) -> (B -> A) -> U)
      substInv (B -> B) (Q B (idfun B)) g (idfun B) (<i> \(b : B) -> (sg b) @ i) h1
 
    rem1 (A : U) (f : A -> B) : P A f = \(g : B -> A) (sg : section A B f g) (rg : retract A B f g) -> 
-          elimEquiv B P rem A (f,gradLemma A B f g sg rg) g sg rg
+          elimEquiv B P rem A (f,isoToEquiv A B f g sg rg) g sg rg
 
 elimIsIso (A : U) (Q : (B : U) -> (A -> B) -> (B -> A) -> U)
          (d : Q A (idfun A) (idfun A)) (B : U) (f : A -> B) (g : B -> A)

diff --git a/experiments/gradLemma.ctt b/experiments/isoToEquiv.ctt
similarity index 96%
rename from experiments/gradLemma.ctt
rename to experiments/isoToEquiv.ctt
index fa01e27f0f15d600fb5adcd8e01521b2d7f344dd..e779d33b5d53992ff73592de8e3b29158dcde0df 100644 (file)
--- a/experiments/gradLemma.ctt
+++ b/experiments/isoToEquiv.ctt
@@ -1,11 +1,9 @@
--- This file contains a proof of the graduate lemma using the old
--- version of equivalence
-module gradLemma where
+-- This file contains a proof of the isoToId using the old version of
+-- equivalence
+module isoToEquiv where
 
 import equiv
 
--- Gradlemma:
-
 lemIso (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)
@@ -56,7 +54,7 @@ lemIso (A B : U) (f : A -> B) (g : B -> A)
                                          , (j = 0) -> s (f (p @ i))
                                          , (j = 1) -> s y ]
 
-gradLemma (A B : U) (f : A -> B) (g : B -> A)
+isoToEquiv (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) : isEquiv A B f = (fCenter,fIsCenter)
   where

diff --git a/experiments/testall.ctt b/experiments/testall.ctt
index 080b0a69dd1bce35194bad9bc00f55b6150a19d7..f0d703d219273d7a4a62c54c8070c86761980ec8 100644 (file)
--- a/experiments/testall.ctt
+++ b/experiments/testall.ctt
@@ -1,6 +1,5 @@
 module testall where
 
-import gradLemma
 import interval
 import uafunext2
 import prop

diff --git a/experiments/univalence.ctt b/experiments/univalence.ctt
index 58d5ae55f6602c1cd45a99877f23a8229d7b17e8..d8a1aaa62ce91da48b4bfcb576ca4235e9e0a7a2 100644 (file)
--- a/experiments/univalence.ctt
+++ b/experiments/univalence.ctt
@@ -1,7 +1,7 @@
 -- The old version of univalence using the old definition of equivalences
 module univalence where
 
-import gradLemma
+import isoToEquiv
 
 transEquivToId (A B : U) (w : equiv A B) : Id U A B =
   <i> glue B [ (i = 1) -> (B,eB)
@@ -36,7 +36,7 @@ idToId (A B : U) (w : equiv A B)
 
 transEquivIsEquiv (A B : U)
   : isEquiv (Id U A B) (equiv A B) (transEquiv A B)
-  = gradLemma (Id U A B) (equiv A B) (transEquiv A B)
+  = isoToEquiv (Id U A B) (equiv A B) (transEquiv A B)
       (transEquivToId A B) (idToId A B) (eqToEq A B)
 
 univalence (A B : U) : equiv (Id U A B) (equiv A B) =
@@ -82,4 +82,4 @@ univalence2 (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) =
     (isEquiv (Id U A B) (equiv A B))
      (canIdToEquiv A B) (transEquiv A B)
      (canIdToEquivIsTransEquiv A B)
-     (transEquivIsEquiv A B)
\ No newline at end of file
+     (transEquivIsEquiv A B)

diff --git a/lectures/lecture4.ctt b/lectures/lecture4.ctt
index add1b7752d52bd94769d415e69c979a5c5037bd3..c0adc64f5c8a89687f97de2ea6f4df3af7ba7fb3 100644 (file)
--- a/lectures/lecture4.ctt
+++ b/lectures/lecture4.ctt
@@ -59,8 +59,8 @@ isPropIsEquiv (A B : U) (f : A -> B) : isProp (isEquiv A B f) =
   \(u0 u1 : isEquiv A B f) ->
   <i> \(y : B) -> isPropIsContr (fiber A B f y) (u0 y) (u1 y) @ i
 
--- The "grad lemma": any isomorphism is an equivalence
-gradLemma (A B : U) (f : A -> B) (g : B -> A)
+-- The "isoToEquiv": any isomorphism is an equivalence
+isoToEquiv (A B : U) (f : A -> B) (g : B -> A)
        (s : (y : B) -> Path B (f (g y)) y)
        (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f =
   \(y:B) -> ((g y,<i>s y@-i),\ (z:fiber A B f y) ->
@@ -167,7 +167,7 @@ ua (A B : U) (e : equiv A B) : Path U A B =
 -- recall: notK : (b : bool) -> Path bool (not (not b)) b = ...
 
 notEquiv : equiv bool bool =
-  (not,gradLemma bool bool not not notK notK)
+  (not,isoToEquiv bool bool not not notK notK)
 
 -- Construct an equality in the universe using Glue
 notEq : Path U bool bool =
@@ -231,7 +231,7 @@ predsucZ : (x : Z) -> Path Z (predZ (sucZ x)) x = split
   inr v -> <i> inr v
 
 sucPathZ : Path U Z Z =
-   <i> Glue Z [ (i = 0) -> (Z,sucZ,gradLemma Z Z sucZ predZ sucpredZ predsucZ)
+   <i> Glue Z [ (i = 0) -> (Z,sucZ,isoToEquiv Z Z sucZ predZ sucpredZ predsucZ)
               , (i = 1) -> (Z,idEquiv Z) ]
 
 -- We can transport along the proof forward and backwards: