From d4d4844b16bd521444bc445dec9cf9d10765deac Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 31 Dec 2015 09:03:46 +0100 Subject: [PATCH] Make aim.ctt compile --- examples/aim.ctt | 86 ++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 76 insertions(+), 10 deletions(-) diff --git a/examples/aim.ctt b/examples/aim.ctt index 4635e41..9608695 100644 --- a/examples/aim.ctt +++ b/examples/aim.ctt @@ -395,7 +395,7 @@ function from A to B: -- This gives a simple proof of subst (called transportf above and in -- UniMath): subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = - transport (maponpaths A U P a b p) e + transport (cong A U P a b p) e -- Transport is defined in the Haskell code as a composition with an @@ -474,19 +474,88 @@ We also want univalence and HITs. Glueing -------------------------------------------------------------------------- -Glueing is a alternative form of univalence for producing non-trivial -equalities from isomorphisms. In particular glueing gives a map from -Iso(A,B) to A = B. This alternative form of univalence is useful for -developing a lot of examples. +Glueing is what enables us to prove univalence by producing +non-trivial equalities from equivalences. In particular glueing gives +a map from Equiv(A,B) to A = B. -} +isContr (A : U) : U = (x : A) * ((y : A) -> Id A x y) + +fiber (A B : U) (f : A -> B) (y : B) : U = + (x : A) * Id B y (f x) + +isEquiv (A B : U) (f : A -> B) : U = + (y : B) -> isContr (fiber A B f y) + +idIsEquiv (A : U) : isEquiv A A (idfun A) = + \(a : A) -> ((a, refl A a) + ,\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) + +-- Using the grad lemma we can transform isomorphisms into equalities. +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) + (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) : + Id (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) + where + rem0 : Id A (g y) x0 = + comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ] + + rem1 : Id A (g y) x1 = + comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ] + + p : Id A x0 x1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 + , (i = 1) -> rem1 ] + + fill0 : Square A (g y) (g (f x0)) (g y) x0 + ( g (p0 @ i)) rem0 ( g y) (t x0) = + comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k + , (i = 0) -> <_> g y + , (j = 0) -> <_> g (p0 @ i) ] + + fill1 : Square A (g y) (g (f x1)) (g y) x1 + ( g (p1 @ i)) rem1 ( g y) (t x1) = + comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k + , (i = 0) -> <_> g y + , (j = 0) -> <_> g (p1 @ i) ] + + fill2 : Square A (g y) (g y) x0 x1 + (<_> g y) p rem0 rem1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 @ j /\ k + , (i = 1) -> rem1 @ j /\ k + , (j = 0) -> <_> g y ] + + sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) + ( g y) ( g (f (p @ i))) + ( g (p0 @ j)) ( g (p1 @ j)) = + comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k + , (i = 1) -> fill1 @ j @ -k + , (j = 0) -> <_> g y + , (j = 1) -> t (p @ i) @ -k ] + + sq1 : Square B y y (f x0) (f x1) + (<_>y) ( f (p @ i)) p0 p1 = + comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + , (i = 1) -> s (p1 @ j) + , (j = 1) -> s (f (p @ i)) + , (j = 0) -> s y ] + +gradLemma (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 = + \ (y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) + + 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 A [ (i = 0) -> (A,idfun A,idfun A,refl A,refl A) - , (i = 1) -> (B,g,f,t,s) ] + glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) + , (i = 1) -> (B,idfun B,idIsEquiv B) ] + + @@ -586,9 +655,6 @@ testNOneZ : Z = transport ( sucIdZ @ - i) zeroZ - - - {- Higher-inductive types (HITs) -------------------------------------------------------------------------- -- 2.34.1