From 3d92424543b9675e05658342349589e5068dd364 Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 17 Jun 2015 17:43:48 +0200 Subject: [PATCH] Finish the proof of univalence --- examples/gradLemma.ctt | 81 ++++++++++++++++++------ examples/univ.ctt | 139 ++++++++++++++++++++++++----------------- 2 files changed, 142 insertions(+), 78 deletions(-) diff --git a/examples/gradLemma.ctt b/examples/gradLemma.ctt index 8634135..1c106d8 100644 --- a/examples/gradLemma.ctt +++ b/examples/gradLemma.ctt @@ -4,30 +4,71 @@ import prelude 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) + (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 ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = (p@i,sq1@i) + Id ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = (p @ i, sq1 @ i) where - rem0 : Id A (g y) x0 = comp A (g (p0 @ i)) [(i=1) -> t x0] - rem1 : Id A (g y) x1 = comp A (g (p1 @ i)) [(i=1) -> t x1] - fill0 : Square A (g y) (g (f x0)) (g (p0 @ i)) (g y) x0 rem0 ((g y)) (t x0) = - comp A (g (p0@i)) [(i=1) -> (t x0)@k/\j ] - fill1 : Square A (g y) (g (f x1)) (g (p1 @ i)) (g y) x1 rem1 ((g y)) (t x1) = - comp A (g (p1@i)) [(i=1) -> (t x1)@k/\j ] - p : Id A x0 x1 = comp A (g y) [(i=0) -> rem0, (i=1) -> rem1] - fill : Square A (g y) (g y) (refl A (g y)) x0 x1 p rem0 rem1 = - comp A (g y) [(i=0) -> (rem0@j/\k), (i=1) -> (rem1@j/\k)] - sq : Square A (g y) (g y) (refl A (g y)) (g (f x0)) (g (f x1)) ((g (f (p@i)))) - (g (p0@i)) (g (p1@i)) = - comp A ((fill@i)@j) [(i=0) -> ((fill0@j)@-k), (i=1)->((fill1@j)@-k),(j=1) -> (t (p@i))@-k] - sq1 : Square B y y (refl B y) (f x0) (f x1) (f (p@i)) p0 p1 = - comp B (f ((sq@i)@j)) [(i=0) -> s (p0@j),(i=1) -> s (p1@j),(j=0) -> s y,(j=1)-> s (f (p@i))] - + rem0 : Id A (g y) x0 = + comp (<_> A) (g (p0 @ i)) [ (i = 0) -> <_> g y, (i = 1) -> t x0 ] + rem1 : Id A (g y) x1 = + comp (<_> A) (g (p1 @ i)) [ (i = 0) -> <_> g y, (i = 1) -> t x1 ] + p : Id A x0 x1 = comp (<_> A) (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ] + + fill0 : Square A (g y) (g (f x0)) ( g (p0 @ i)) (g y) x0 rem0 ( g y) (t x0) = + comp (<_> A) (g (p0@i)) [ (i = 0) -> <_> g y + , (i = 1) -> t x0 @ j /\ k + , (j = 0) -> <_> g (p0 @ i) ] + + fill1 : Square A (g y) (g (f x1)) ( g (p1 @ i)) (g y) x1 rem1 ( g y) (t x1) = + comp (<_> A) (g (p1@i)) [ (i = 0) -> <_> g y + , (i = 1) -> t x1 @ j /\ k + , (j = 0) -> <_> g (p1 @ i) ] + + fill2 : Square A (g y) (g y) (<_> g y) x0 x1 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 y) (g (f x0)) (g (f x1)) ( g (f (p @ i))) + ( g (p0 @ i)) ( g (p1 @ i)) = + 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 (<_> y) (f x0) (f x1) ( f (p @ i)) p0 p1 = + comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + , (i = 1) -> s (p1 @ j) + , (j = 0) -> s y + , (j = 1) -> s (f (p @ i)) ] + + +-- 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 ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = (p@i,sq1@i) +-- where +-- rem0 : Id A (g y) x0 = comp A (g (p0 @ i)) [(i=1) -> t x0] +-- rem1 : Id A (g y) x1 = comp A (g (p1 @ i)) [(i=1) -> t x1] +-- fill0 : Square A (g y) (g (f x0)) (g (p0 @ i)) (g y) x0 rem0 ((g y)) (t x0) = +-- comp A (g (p0@i)) [(i=1) -> (t x0)@k/\j ] +-- fill1 : Square A (g y) (g (f x1)) (g (p1 @ i)) (g y) x1 rem1 ((g y)) (t x1) = +-- comp A (g (p1@i)) [(i=1) -> (t x1)@k/\j ] +-- p : Id A x0 x1 = comp A (g y) [(i=0) -> rem0, (i=1) -> rem1] +-- fill : Square A (g y) (g y) (refl A (g y)) x0 x1 p rem0 rem1 = +-- comp A (g y) [(i=0) -> (rem0@j/\k), (i=1) -> (rem1@j/\k)] +-- sq : Square A (g y) (g y) (refl A (g y)) (g (f x0)) (g (f x1)) ((g (f (p@i)))) +-- (g (p0@i)) (g (p1@i)) = +-- comp A ((fill@i)@j) [(i=0) -> ((fill0@j)@-k), (i=1)->((fill1@j)@-k),(j=1) -> (t (p@i))@-k] +-- sq1 : Square B y y (refl B y) (f x0) (f x1) (f (p@i)) p0 p1 = +-- comp B (f ((sq@i)@j)) [(i=0) -> s (p0@j),(i=1) -> s (p1@j),(j=0) -> s y,(j=1)-> s (f (p@i))] + -- special case corrIso (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) + (t : (x:A) -> Id A (g (f x)) x) (x0:A) : - Id ((x:A) * Id B (f x0) (f x)) (x0,refl B (f x0)) (g (f x0),((s (f x0))@-i)) = - lemIso A B f g s t (f x0) x0 (g (f x0)) (refl B (f x0)) (((s (f x0))@-i)) + Id ((x:A) * Id B (f x0) (f x)) (x0,refl B (f x0)) (g (f x0),((s (f x0))@-i)) = + lemIso A B f g s t (f x0) x0 (g (f x0)) (refl B (f x0)) (((s (f x0))@-i)) diff --git a/examples/univ.ctt b/examples/univ.ctt index 536d8ee..9a0e1b1 100644 --- a/examples/univ.ctt +++ b/examples/univ.ctt @@ -1,6 +1,5 @@ module univ where - -- Some things from the prelude Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1 @@ -27,7 +26,6 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d where T (z : singl A a) : U = C (z.1) (z.2) - compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = comp (<_>A) (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ] @@ -44,34 +42,32 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x)) (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1 = \ (x:A) -> (h x (f0 x) (f1 x)) @ i -lemSig (A : U) (B : A->U) (pB : (x : A) -> prop (B x)) (u v : (x:A) * B x) (p : Id A u.1 v.1) : - Id ((x:A) * B x) u v = (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i) - -propSig (A : U) (B : A-> U) (pA : prop A) (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) - : Id ((x:A) * B x) t u - = lemSig A B pB t u (pA t.1 u.1) +lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x)) + (u v : (x:A) * B x) (p : Id A u.1 v.1) : + Id ((x:A) * B x) u v = + (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i) +propSig (A : U) (B : A -> U) (pA : prop A) + (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) : + Id ((x:A) * B x) t u = + lemSig A B pB t u (pA t.1 u.1) propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q = - comp (<_>A) a [ (i=0) -> h a a - , (i=1) -> h a b - , (j=0) -> h a (p @ i) - , (j=1) -> h a (q @ i)] - + comp (<_> A) a [ (i = 0) -> h a a + , (i = 1) -> h a b + , (j = 0) -> h a (p @ i) + , (j = 1) -> h a (q @ i)] isContr (A : U) : U = (x : A) * ((y : A) -> Id A x y) propIsContr (A : U) : prop (isContr A) = lemProp (isContr A) rem where - rem (t : isContr A) : prop (isContr A) = - propSig A T pA pB - where - T (x : A) : U = (y : A) -> Id A x y - pA (x y : A) : Id A x y = compId A x t.1 y ( t.2 x @ -i) (t.2 y) - pB (x : A) : prop (T x) = - propPi A (\ (y : A) -> Id A x y) (propSet A pA x) - - + rem (t : isContr A) : prop (isContr A) = propSig A T pA pB + where + T (x : A) : U = (y : A) -> Id A x y + pA (x y : A) : Id A x y = compId A x t.1 y ( t.2 x @ -i) (t.2 y) + pB (x : A) : prop (T x) = + propPi A (\ (y : A) -> Id A x y) (propSet A pA x) ---------------------------------------------------------------------- @@ -82,44 +78,72 @@ isEquiv (A B : U) (f : A -> B) : U = (s : (y : B) -> fiber A B f y) * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w) -equiv (A B : U) : U = - (f : A -> B) - * isEquiv A B f - +equiv (A B : U) : U = (f : A -> B) * isEquiv A B f -- Gradlemma: -Square (A : U) (a0 a1 : A) (u : Id A a0 a1) - (b0 b1 : A) (v : Id A b0 b1) + +-- u +-- a0 -----> a1 +-- | | +-- r0 | | r1 +-- | | +-- V V +-- b0 -----> b1 +-- v +Square (A : U) (a0 a1 b0 b1 : A) + (u : Id A a0 a1) (v : Id A b0 b1) (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U = IdP ( (IdP ( A) (u @ i) (v @ i))) r0 r1 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 ((x:A) * Id B y (f x)) (x0,p0) (x1,p1) = (p @ i, sq1 @ i) - where - rem0 : Id A (g y) x0 = comp (<_> A) (g (p0 @ i)) [(i=0) -> <_> g y,(i=1) -> t x0] - rem1 : Id A (g y) x1 = comp (<_> A) (g (p1 @ i)) [(i=0) -> <_> g y,(i=1) -> t x1] - fill0 : Square A (g y) (g (f x0)) (g (p0 @ i)) (g y) x0 rem0 ((g y)) (t x0) = undefined - -- comp (<_> A) (g (p0@i)) [(i=1) -> (t x0)@k/\j ] - fill1 : Square A (g y) (g (f x1)) (g (p1 @ i)) (g y) x1 rem1 ((g y)) (t x1) = undefined --- comp (<_> A) (g (p1@i)) [(i=1) -> (t x1)@k/\j ] - p : Id A x0 x1 = comp (<_> A) (g y) [(i=0) -> rem0, (i=1) -> rem1] - fill2 : Square A (g y) (g y) (refl A (g y)) x0 x1 p rem0 rem1 = undefined --- comp (<_> A) (g y) [(i=0) -> (rem0@j/\k), (i=1) -> (rem1@j/\k)] - sq : Square A (g y) (g y) (refl A (g y)) (g (f x0)) (g (f x1)) ((g (f (p@i)))) - (g (p0@i)) (g (p1@i)) = undefined --- comp (<_> A) ((fill2@i)@j) [(i=0) -> ((fill0@j)@-k), (i=1)->((fill1@j)@-k),(j=1) -> (t (p@i))@-k] - sq1 : Square B y y (refl B y) (f x0) (f x1) (f (p@i)) p0 p1 = - comp (<_>B) (f ((sq@i)@j)) [(i=0) -> s (p0@j),(i=1) -> s (p1@j),(j=0) -> s y,(j=1)-> s (f (p@i))] - --- lemIso is stated the wrong way around for our definition of fiber -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 (f x0) y) (p1 : Id B (f x1) y) : - Id (fiber A B f y) (x0,p0) (x1,p1) = undefined + (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 (f x0) y) (p1 : Id B (f x1) y) : + Id (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) + where + rem0 : Id A x0 (g y) = + comp (<_> A) (g (p0 @ i)) [ (i = 0) -> t x0, (i = 1) -> <_> g y ] + + rem1 : Id A x1 (g y) = + comp (<_> A) (g (p1 @ i)) [ (i = 0) -> t x1, (i = 1) -> <_> g y ] + + p : Id A x0 x1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 @ -j + , (i = 1) -> rem1 @ -j ] + + + fill0 : Square A (g (f x0)) (g y) x0 (g y) + ( g (p0 @ i)) rem0 (t x0) ( g y) = + comp (<_> A) (g (p0 @ i)) [ (i = 0) -> t x0 @ j /\ k + , (i = 1) -> <_> g y + , (j = 0) -> <_> g (p0 @ i) ] + + fill1 : Square A (g (f x1)) (g y) x1 (g y) + ( g (p1 @ i)) rem1 (t x1) ( g y) = + comp (<_> A) (g (p1 @ i)) [ (i = 0) -> t x1 @ j /\ k + , (i = 1) -> <_> g y + , (j = 0) -> <_> g (p1 @ i) ] + + fill2 : Square A x0 x1 (g y) (g y) + p (<_> g y) rem0 rem1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 @ j \/ -k + , (i = 1) -> rem1 @ j \/ -k + , (j = 1) -> <_> g y ] + + sq : Square A (g (f x0)) (g (f x1)) (g y) (g y) + ( g (f (p @ i))) ( g y) + ( g (p0 @ j)) ( g (p1 @ j)) = + comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k + , (i = 1) -> fill1 @ j @ -k + , (j = 1) -> <_> g y + , (j = 0) -> t (p @ i) @ -k ] + + sq1 : Square B (f x0) (f x1) y y + ( f (p @ i)) (<_> y) p0 p1 = + comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + , (i = 1) -> s (p1 @ j) + , (j = 0) -> s (f (p @ i)) + , (j = 1) -> s y ] gradLemma (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Id B (f (g y)) y) @@ -127,17 +151,16 @@ gradLemma (A B : U) (f : A -> B) (g : B -> A) where fCenter (y : B) : fiber A B f y = (g y,s y) 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 + lemIso A B f g s t y (fCenter y).1 w.1 (fCenter y).2 w.2 -- The identity function is an equivalence idFun (A : U) (a : A) : A = a -idCenter (A : U) (y : A) : fiber A A (idFun A) y = - (y, refl A y) +idCenter (A : U) (y : A) : fiber A A (idFun A) y = (y, refl A y) -- TODO: redifine fiber so this gets nicer? -idIsCenter (A : U) (y : A) (w : fiber A A (idFun A) y) +idIsCenter (A : U) (y : A) (w : fiber A A (idFun A) y) : Id (fiber A A (idFun A) y) (idCenter A y) w = (w.2 @ -i, w.2 @ j \/ -i) -- 2.34.1