From 66b30d8b4eff7efff38010377e06b910172bbe2e Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 16 Jun 2015 22:27:34 +0200 Subject: [PATCH] A proof of univalence (wip) --- examples/univ.ctt | 309 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 309 insertions(+) create mode 100644 examples/univ.ctt diff --git a/examples/univ.ctt b/examples/univ.ctt new file mode 100644 index 0000000..5b7beeb --- /dev/null +++ b/examples/univ.ctt @@ -0,0 +1,309 @@ +module univ where + + +-- Some things from the prelude + +Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1 + +refl (A : U) (a : A) : Id A a a = a + +mapOnPath (A B : U) (f : A -> B) (a b : A) + (p : Id A a b) : Id B (f a) (f b) = f (p @ i) + +funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) + (p : (x : A) -> Id (B x) (f x) (g x)) : + Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i + +subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = + comp (mapOnPath A U P a b p) e [] + +singl (A : U) (a : A) : U = (x : A) * Id A a x + +contrSingl (A : U) (a b : A) (p : Id A a b) : + Id (singl A a) (a,refl A a) (b,p) = (p @ i, p @ i/\j) + +J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) + (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p = + 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 ] + +prop (A : U) : U = (a b : A) -> Id A a b + +lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) : + (a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1 = + J A a (\ (a1 : A) (p : Id A a a1) -> (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1) rem + where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a + +lemProp (A : U) (h : A -> prop A) : prop A = \ (a : A) -> h a a + +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) + + +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)] + + +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) + + + +---------------------------------------------------------------------- + +fiber (A B : U) (f : A -> B) (y : B) : U = + (x : A) * Id B (f x) y + +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 + +-- 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) + +-- TODO: redifine fiber so this gets nicer? +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) + +idIsEquiv (A : U) : isEquiv A A (idFun A) = (idCenter A,idIsCenter A) + +idEquiv (A : U) : equiv A A = (idFun A, idIsEquiv A) + + +-- Transport is an equivalence +-- NB: The proof is taken from the output of a comp U +trans (A B : U) (p : Id U A B) (a : A) : B = comp p a [] + +transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y = + (comp ( p @ -i0) y [] + , comp p (comp ( p @ -i0) y []) + [ (i0 = 0) -> comp ( p @ (i1 /\ i2)) (comp ( p @ -i0) y []) + [ (i1 = 0) -> comp ( p @ -i0) y [] ] + , (i0 = 1) -> comp ( p @ (i1 \/ -i2)) y [ (i1 = 1) -> y ] ]) + +transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y) + : Id (fiber A B (trans A B p) y) (transCenter A B p y) w + = + ( comp ( p @ -i1) (w.2 @ -i0) + [ (i0 = 0) -> comp ( p @ (-i1 \/ -i2)) y [ (i1 = 0) -> y ] + , (i0 = 1) -> comp ( p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> w.1 ] ] + , comp ( p @ i2) + (comp ( p @ -i2) (w.2 @ (-i0 \/ i1)) + [ (i0 = 0) -> comp ( p @ (-i2 \/ -i3)) y [ (i2 = 0) -> y ] + , (i0 = 1)(i1 = 0) -> + comp ( p @ (-i2 /\ i3)) (w.1) + [ (i2 = 1) -> w.1 ] + , (i1 = 1) -> comp ( p @ (-i2 \/ -i3)) y [ (i2 = 0) -> y ] ]) + [ (i0 = 0) -> comp ( p @ (i2 /\ i3)) + (comp ( p @ -i0) y [ ]) + [ (i1 = 0) -> + comp ( p @ (i2 /\ i3 /\ i4)) + (comp ( p @ -i0) y [ ]) + [ (i2 = 0) -> comp ( p @ -i0) y [ ] + , (i3 = 0) -> comp ( p @ -i0) y [ ] ] + , (i1 = 1) -> + comp ( p @ ((i2 /\ i3) \/ -i4)) y + [ (i2 = 1)(i3 = 1) -> y ] + , (i2 = 0) -> comp ( p @ -i0) y [ ] ] + , (i0 = 1) -> + comp ( p @ (i2 \/ -i3)) (w.2 @ i1) + [ (i1 = 0) -> + comp ( p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1) + [ (i2 = 0)(i3 = 1) -> w.1 ] + , (i1 = 1) -> + comp ( p @ (i2 \/ -i3 \/ -i4)) y + [ (i2 = 1) -> y, (i3 = 0) -> y ] + , (i2 = 1) -> w.2 @ i1 ] + , (i1 = 0) -> + comp ( p @ (i2 /\ i3)) + (comp ( p @ -i1) (w.2 @ -i0) + [ (i0 = 0) -> + comp ( p @ (-i1 \/ -i2)) y [ (i1 = 0) -> y ] + , (i0 = 1) -> + comp ( p @ (-i1 /\ i2)) (w.1) + [ (i1 = 1) -> w.1 ] + ]) + [ (i2 = 0) -> + comp ( p @ -i1) (w.2 @ -i0) + [ (i0 = 0) -> + comp ( p @ (-i1 \/ -i2)) y + [ (i1 = 0) -> y ] + , (i0 = 1) -> + comp ( p @ (-i1 /\ i2)) (w.1) + [ (i1 = 1) -> w.1 ] + ] + ] + , (i1 = 1) -> comp ( p @ (i2 \/ -i3)) y [ (i2 = 1) -> y ] ] + ) + +transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) = + (transCenter A B p,transIsCenter A B p) + +transEquiv (A B : U) (p : Id U A B) : equiv A B = + (trans A B p,transIsEquiv A B p) + +transDelta (A : U) : equiv A A = transEquiv A A (<_> A) + +transEquivToId (A B : U) (w : equiv A B) : Id U A B = + glue B [ (i=1) -> (B,transDelta B), (i=0) -> (A,w) ] + +eqToEq (A B : U) (p : Id U A B) + : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p + = glue B + [ (i=0) -> (A,transEquiv A B p) + , (i=1) -> (B,transEquiv B B (<_> B)) + , (j=1) -> (p@i,transEquiv (p@i) B ( p @ (i \/ k)))] + +eqToEq' (A : U) : (B : U) (p : Id U A B) + -> Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p + = J U A + (\ (B : U) (p : Id U A B) -> + Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p) + ( glue A + [ (i=0) -> (A,transDelta A) + , (i=1) -> (A,transDelta A) + , (j=1) -> (A,transDelta A)]) + +transIdFun (A B : U) (w : equiv A B) + : Id (A -> B) (trans A B (transEquivToId A B w)) w.1 = + \(a : A) -> let b : B = w.1 a + in addf (f (f (f b))) b (addf (f (f b)) b (addf (f b) b (trf b))) @ i + where f (b : B) : B = comp (<_> B) b [] + trf (b : B) : Id B (f b) b = + fill (<_> B) b [] @ -i + addf (b b' : B) : Id B b b' -> Id B (f b) b' = + compId B (f b) b b' (trf b) + + +propIsEquiv (A B : U) (f : A -> B) + : prop (isEquiv A B f) = lemProp (isEquiv A B f) lem + where + isEqf : U = isEquiv A B f + fibf : (y : B) -> U = fiber A B f + center : U = (y : B) -> fibf y + isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w + lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc + where + fibprop (y : B) (u v : fibf y) : Id (fibf y) u v = + compId (fibf y) u (fe.1 y) v ( fe.2 y u @ -i) (fe.2 y v) + pc : prop center = propPi B fibf fibprop + pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h = + \ (y : B) (w : fibf y) -> + propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i + +idToId (A B : U) (w : equiv A B) + : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w + = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) + (transEquiv A B (transEquivToId A B w)) w + (transIdFun A B w) + + + +-- Any equality defines an equivalence +idToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B = + J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A) + +equivId + (A B : U) + (f : A -> B) + (s : (y : B) -> fiber A B f y) + (t : (y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w) + : Id U A B = + glue B + [ (i=1) -> (B,idEquiv B) + , (i=0) -> (A,f,s,t)] + +equivToId (A B : U) (w : equiv A B) : Id U A B = + glue B [ (i=1) -> (B,idEquiv B), (i=0) -> (A,w) ] + + +foo (A B : U) (w : equiv A B) (a : A) : B = (idToEquiv A B (equivToId A B w)).1 a + +testfun (A B : U) (w : equiv A B) + : Id (A -> B) (idToEquiv A B (equivToId A B w)).1 w.1 = + \(a : A) -> let b : B = w.1 (fill (<_> A) a [] @ -i) + in (addf (f (f b)) b (addf (f b) b (trf b))) @ i + where p : A -> B = (idToEquiv A B (equivToId A B w)).1 + f (b : B) : B = comp (<_> B) b [] + trf (b : B) : Id B (f b) b = + fill (<_> B) b [] @ -i + addf (b b' : B) : Id B b b' -> Id B (f b) b' = + compId B (f b) b b' (trf b) + +test (A B : U) (w : equiv A B) : Id (equiv A B) (idToEquiv A B (equivToId A B w)) w = + lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) + (idToEquiv A B (equivToId A B w)) w + (testfun A B w) + +test2 (A : U) : Id (equiv A A) (idToEquiv A A (equivToId A A (idEquiv A))) (idEquiv A) = + test A A (idEquiv A) + +{- +equivToId (A B : U) (w : equiv A B) : Id U A B = + glue B [ (i=1) -> (B,idEquiv B), (i=0) -> (A,w) ] + --equivId A B w.1 w.2.1 w.2.2 + +test (A : U) : Id U A A = (equivToId A A (idToEquiv A A (refl U A))) + +test2 (A : U) (a : A) : A = comp (test A) a [] + +want (A : U) : Id (Id U A A) (test A) (equivToId A A (idEquiv A)) = undefined + +test3 (A : U) (a : A) : A = comp (equivToId A A (idEquiv A)) a [] + +test4 (A B : U) (w : equiv A B) (a : A) : B = comp (equivToId A B w) a [] + +test4nf (A B : U) (w : equiv A B) (a : A) : B = + comp ( B) (comp ( B) (comp ( B) (w.1 a) [ ]) [ ]) [ ] + + +ormaybe (A A : U) : Id (equiv A A) (idEquiv A) (idToEquiv A A (refl U A)) = + undefined + +-- eqToEq (A : U) +-- : (B : U) (p : Id U A B) -> +-- Id (Id U A B) (equivToId A B (idToEquiv A B p)) p = +-- J U A +-- (\ (B : U) (p : Id U A B) -> +-- Id (Id U A B) (equivToId A B (idToEquiv A B p)) p) +-- ? +-- -- ( glue A +-- -- [ (i=0) -> (A,idFun A,idCenter A,idIsCenter A) +-- -- , (i=1) -> (A,idFun A,idCenter A,idIsCenter A) +-- -- , (j=1) -> (A,idFun A,idCenter A,idIsCenter A)]) + + + +-} \ No newline at end of file -- 2.34.1