From a331f1d355c5d2fc608a59c1cbbf016ea09d6deb Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Fri, 11 Aug 2017 19:28:50 +0200 Subject: [PATCH] rename gradLemma to isoToEquiv --- Eval.hs | 12 ++++---- examples/bool.ctt | 4 +-- examples/category.ctt | 20 ++++++------- examples/equiv.ctt | 12 ++++---- examples/idtypes.ctt | 2 +- examples/subset.ctt | 2 +- examples/torsor.ctt | 28 +++++++++---------- examples/univalence.ctt | 4 +-- experiments/{gradLemma.ctt => isoToEquiv.ctt} | 10 +++---- experiments/testall.ctt | 1 - experiments/univalence.ctt | 6 ++-- lectures/lecture4.ctt | 8 +++--- 12 files changed, 53 insertions(+), 56 deletions(-) rename experiments/{gradLemma.ctt => isoToEquiv.ctt} (96%) diff --git a/Eval.hs b/Eval.hs index e013605..25f09c5 100644 --- 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 89b365d..0759a62 100644 --- 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 = 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 71ff7f3..34dfc87 100644 --- 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 ( 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)->\(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)->(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))->\(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)->(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))->\(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)->\(a:A)->retEq (B0 a) (B1 a) (e a) (g a)@i) (\(f:(a:A)->B0 a)->\(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 ((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 ( 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 db4b75b..d5a80c0 100644 --- 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) (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,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 = - Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) + 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) -> a) (\(a : A) -> a) +idIsEquivIsoToEquiv (A : U) : isEquiv A A (idfun A) = + isoToEquiv A A (idfun A) (idfun A) (\(a : A) -> a) (\(a : A) -> a) diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt index be8c80f..913e6a9 100644 --- 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) -> pathToIdToPath U A B p @ - i) (\(p : Id U A B) -> idToPathToId U A B p @ - i) diff --git a/examples/subset.ctt b/examples/subset.ctt index 0df6500..2090295 100644 --- 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 ( p @ i -> A) (\ (x : X) -> f' (g (h x))) f) q : P B' g' - = elimEquiv B P ( B, f) B' (g', gradLemma B' B g' g s t) + = elimEquiv B P ( B, 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 c9faa9e..70133c3 100644 --- a/examples/torsor.ctt +++ b/examples/torsor.ctt @@ -8,7 +8,7 @@ import helix isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isEquiv B C G) : isEquiv A C (\(x : A) -> G (F x)) - = gradLemma A C (\(x : A) -> G (F x)) (\(x : C) -> (ef (eg x).1.1).1.1) + = isoToEquiv A C (\(x : A) -> G (F x)) (\(x : C) -> (ef (eg x).1.1).1.1) (\(x : C) -> compPath C (G (F (ef (eg x).1.1).1.1)) (G (eg x).1.1) x ( G (retEq A B (F, ef) (eg x).1.1 @ i)) (retEq B C (G, eg) x)) (\(x : A) -> compPath A ((ef (eg (G (F x))).1.1).1.1) (ef (F x)).1.1 x @@ -16,7 +16,7 @@ isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isE isEquivComp' (A B C : U) (F : A -> B) (G : C -> B) (ef : isEquiv A B F) (eg : isEquiv C B G) : isEquiv A C (\(x : A) -> (eg (F x)).1.1) - = gradLemma A C (\(x : A) -> (eg (F x)).1.1) (\(x : C) -> (ef (G x)).1.1) + = isoToEquiv A C (\(x : A) -> (eg (F x)).1.1) (\(x : C) -> (ef (G x)).1.1) (\(x : C) -> compPath C (eg (F (ef (G x)).1.1)).1.1 (eg (G x)).1.1 x ( (eg (retEq A B (F, ef) (G x) @ i)).1.1) (secEq C B (G, eg) x)) (\(x : A) -> compPath A ((ef (G (eg (F x)).1.1)).1.1) (ef (F x)).1.1 x @@ -96,7 +96,7 @@ lemPathPSet2 (A B : U) (ASet : set A) (p1 : Path U A B) (lemPathPSet A B ASet p1) -isEquivPath (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x) +isEquivPath (A : U) : isEquiv A A (\(x : A) -> x) = isoToEquiv A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x) 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 = transport @@ -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) 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)) isContrProp (A : U) (p : isContr A) (x y : A) : Path A x y = compPath A x p.1 y ( p.2 x @ -i) (p.2 y) @@ -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 ( isContr (hole4@i)) (lem2 A x) contrEquiv (A B : U) (aC : isContr A) (bC : isContr B) : equiv A B - = (\(_ : A) -> bC.1, gradLemma A B (\(_ : A) -> bC.1) (\(_ : B) -> aC.1) (\(x : B) -> bC.2 x) (\(x : A) -> aC.2 x)) + = (\(_ : A) -> bC.1, isoToEquiv A B (\(_ : A) -> bC.1) (\(_ : B) -> aC.1) (\(x : B) -> bC.2 x) (\(x : A) -> aC.2 x)) 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 where @@ -442,7 +442,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Path U (BZSet BA) (BZSet BB)) * PathP ( p@i AEquiv BEquiv ( BZEquiv (q2@i)) ( BZEquiv (q@i)) hole : Path (Path BZ BA BB) q2 q = (p@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i))) hole : equiv ((p : Path U (BZSet BA) (BZSet BB)) * PathP ( p@i -> p@i) (BZS BA) (BZS BB)) (Path BZ BA BB) - = (F, gradLemma ((p : Path U (BZSet BA) (BZSet BB)) * PathP ( p@i -> p@i) (BZS BA) (BZS BB)) (Path BZ BA BB) F G FG GF) + = (F, isoToEquiv ((p : Path U (BZSet BA) (BZSet BB)) * PathP ( p@i -> p@i) (BZS BA) (BZS BB)) (Path BZ BA BB) F G FG GF) 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 inl n -> lem2Aux n @@ -470,7 +470,7 @@ lem2' (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Path A (shift.2 (action A ZBZ : BZ = (Z, (hinhpr Z zeroZ, (ZShift, ZEquiv))) where - ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) + ZShift : equiv Z Z = (sucZ, isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) plus : Z -> Z -> Z = action Z ZShift plusCommZero : (y : Z) -> Path Z (plus zeroZ y) (plus y zeroZ) = split inl u -> hole u @@ -606,14 +606,14 @@ BZequivBZ' : Path U BZ BZ' = isoPath BZ BZ' F G FG GF where SHIFT : isEquiv A.1.1 A.1.1 A.1.2 = A.2 (isEquiv A.1.1 A.1.1 A.1.2, propIsEquiv A.1.1 A.1.1 A.1.2) - (\(a : Path AA A.1 (Z, sucZ)) -> transport ( isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ)) - ZEquiv : (x : Z) -> isEquiv Z Z (action Z (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) x) = BZEquiv ZBZ + (\(a : Path AA A.1 (Z, sucZ)) -> transport ( isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (isoToEquiv Z Z sucZ predZ sucpredZ predsucZ)) + ZEquiv : (x : Z) -> isEquiv Z Z (action Z (sucZ, isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) x) = BZEquiv ZBZ hole (a : Path AA A.1 (Z, sucZ)) - : PathP ( isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ) SHIFT + : PathP ( isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) SHIFT = lemPathPProp (isEquiv Z Z sucZ) (isEquiv A.1.1 A.1.1 A.1.2) (propIsEquiv Z Z sucZ) - ( isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (gradLemma Z Z sucZ predZ sucpredZ predsucZ) SHIFT + ( isEquiv (a@-i).1 (a@-i).1 (a@-i).2) (isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) SHIFT ZEquivEq (a : Path AA A.1 (Z, sucZ)) - : Path U ((x : Z) -> isEquiv Z Z (action Z (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ) x)) + : Path U ((x : Z) -> isEquiv Z Z (action Z (sucZ, isoToEquiv Z Z sucZ predZ sucpredZ predsucZ) x)) ((x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x)) = (x : (a@-i).1) -> isEquiv Z (a@-i).1 (action (a@-i).1 ((a@-i).2, hole a @ i) x) EQUIV : (x : A.1.1) -> isEquiv Z A.1.1 (action A.1.1 (A.1.2, SHIFT) x) @@ -711,7 +711,7 @@ multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv))) opaque FG 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) opaque GF - 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)) + 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)) hole : (y : Z) -> Path (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) y) (decodeZ ZBZ y) = split inl u -> hole0 u 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 @@ -735,7 +735,7 @@ multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv))) (decodeLoop (inr n)) transparent decodeZ TEquiv''' : isEquiv Z (Path BZ ZBZ ZBZ) (action (Path BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ)) - = transport ( isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (gradLemma Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ)) + = transport ( isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (isoToEquiv Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ)) TEquiv'' (b : BZSet B) (x : Path BZ ZBZ B) : isEquiv Z (Path BZ ZBZ B) (action (Path BZ ZBZ B) (TShift ZBZ B) x) = 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)) TEquiv''' B x diff --git a/examples/univalence.ctt b/examples/univalence.ctt index a662d99..70bf026 100644 --- 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) ( \(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 fa01e27..e779d33 100644 --- 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 080b0a6..f0d703d 100644 --- 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 58d5ae5..d8a1aaa 100644 --- 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 = 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 add1b77..c0adc64 100644 --- 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) -> \(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,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 -> inr v sucPathZ : Path U Z Z = - Glue Z [ (i = 0) -> (Z,sucZ,gradLemma Z Z sucZ predZ sucpredZ predsucZ) + 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: -- 2.34.1