From: Anders Date: Thu, 18 Jun 2015 16:23:39 +0000 (+0200) Subject: Cleaning and reorganization of files X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4df26701dfe05d5eba09655812e79036662190e3;p=cubicaltt.git Cleaning and reorganization of files --- diff --git a/examples/add.ctt b/examples/add.ctt deleted file mode 100644 index 1fa272c..0000000 --- a/examples/add.ctt +++ /dev/null @@ -1,53 +0,0 @@ -module add where - -import nat - -add (a : nat) : nat -> nat = split - zero -> a - suc n -> suc (add a n) - -add_zero : (n : nat) -> Id nat (add zero n) n = split - zero -> zero - suc n -> suc (add_zero n @ i) - -add_suc (a:nat) : (n : nat) -> Id nat (add (suc a) n) (suc (add a n)) = split - zero -> suc a - suc m -> suc (add_suc a m @ i) - -add_comm (a : nat) : (n : nat) -> Id nat (add a n) (add n a) = split - zero -> add_zero a @ -i - suc m -> comp nat (suc (add_comm a m @ i)) [ (i = 0) -> suc (add a m), - (i = 1) -> add_suc m a @ -j] - -assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = split - zero -> add a b - suc c1 -> suc (assocAdd a b c1@i) - - --- test (A:U) (a b c d e : A) (p:Id A a b) (q:Id A b c) (r:Id A c d) (s:Id A d e) : Id A a e = --- comp A (p@i) [ (i=1) -> comp A (q@i) [ (i=1) -> comp A (r@i) [ (i=1) -> s]]] - --- data tree = leaf | bin (t0 t1:tree) - --- swap : tree -> tree = split --- leaf -> leaf --- bin t0 t1 -> bin (swap t1) (swap t0) - --- lem : (t:tree) -> Id tree (swap (swap t)) t = split --- leaf -> leaf --- bin t0 t1 -> bin (lem t0@i) (lem t1@i) - --- pred : nat -> nat = split --- zero -> zero --- suc n -> n - --- simplAdd (b c :nat) : (a : nat) -> Id nat (add b a) (add c a) -> Id nat b c = split --- zero -> \ (h:Id nat b c) -> h --- suc a1 -> \ (h : Id nat (suc (add b a1)) (suc (add c a1))) -> simplAdd b c a1 (pred (h@i)) - --- corSimplAdd (b c a :nat) (h: Id nat (add a b) (add a c)) : Id nat b c = simplAdd b c a rem --- where rem : Id nat (add b a) (add c a) = --- comp nat ((add_comm b a)@i) [(i=1) -> comp nat (h@i) [(i=1) -> add_comm a c]] - - --- leq (b c:nat) : U = (a : nat) * Id nat (add a b) c \ No newline at end of file diff --git a/examples/bool.ctt b/examples/bool.ctt index 299ba60..ff1a722 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -1,6 +1,6 @@ module bool where -import prelude +import gradLemma data bool = false | true @@ -15,7 +15,7 @@ negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split negBoolEq : Id U bool bool = isoId bool bool negBool negBool negBoolK negBoolK -test : bool = trans bool bool negBoolEq true +testFalse : bool = transport negBoolEq true data F2 = zeroF2 | oneF2 @@ -64,8 +64,8 @@ test4 : Id U bool bool = negNegEq @ i kanBool : Id U bool bool = kan U bool bool bool bool negBoolEq negBoolEq negBoolEq -squareBoolF2 : Square U bool bool (refl U bool) bool F2 - boolEqF2 (refl U bool) boolEqF2 = +squareBoolF2 : Square U bool bool bool F2 (refl U bool) + boolEqF2 (refl U bool) boolEqF2 = boolEqF2 @ i /\ j test5 : IdP boolEqF2 true oneF2 = diff --git a/examples/equiv.ctt b/examples/equiv.ctt index ef097f2..036a0db 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -2,67 +2,188 @@ module equiv where import prelude -isContr (A : U) : U = and (prop A) A - -fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x) - -lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem - where F : U = fiber A A (\ (x:A) -> x) a - rem (u v:F) : Id F u v = (rem1 @ i,rem2 @ i) - where x : A = u.1 - p : Id A a x = u.2 - y : A = v.1 - q : Id A a y = v.2 - rem1 : Id A x y = comp A a [(i=0) -> p,(i=1) -> q] - rem2 : IdP (Id A a (rem1@i)) p q = comp A a [(i=0) -> p@(j/\l),(i=1) -> q@(j/\l)] - -lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = - \ (u v:and A B) -> ((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i) - -isContrProp (A:U) : prop (isContr A) = - lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h) - -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) -> (lemIdFib A a,(a,refl A a)) - -propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f) - = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y)) - -isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = - isoId A B f g (\ (y:B) -> (s y)@-i) t - where - rem1 (y:B) : prop (fiber A B f y) = (is y).1 - rem2 (y:B) : fiber A B f y = (is y).2 - g (y:B) : A = (rem2 y).1 - s (y:B) : Id B y (f (g y)) = (rem2 y).2 - rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x) - rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = - rem1 (f x) (g (f x),rem3 x) (x,refl B (f x)) - t (x:A) : Id A (g (f x)) x = ((rem4 x)@i).1 +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 + +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 + + +-- The identity function is an equivalence +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 = transport 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) + + + + + + + + +-- Alternative definitions: + +-- isContr (A : U) : U = and (prop A) A + +-- fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x) + +-- lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem +-- where F : U = fiber A A (\ (x:A) -> x) a +-- rem (u v:F) : Id F u v = (rem1 @ i,rem2 @ i) +-- where x : A = u.1 +-- p : Id A a x = u.2 +-- y : A = v.1 +-- q : Id A a y = v.2 +-- rem1 : Id A x y = comp A a [(i=0) -> p,(i=1) -> q] +-- rem2 : IdP (Id A a (rem1@i)) p q = comp A a [(i=0) -> p@(j/\l),(i=1) -> q@(j/\l)] + +-- lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = +-- \ (u v:and A B) -> ((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i) + +-- isContrProp (A:U) : prop (isContr A) = +-- lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h) + +-- 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) -> (lemIdFib A a,(a,refl A a)) + +-- propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f) +-- = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y)) + +-- isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = +-- isoId A B f g (\ (y:B) -> (s y)@-i) t +-- where +-- rem1 (y:B) : prop (fiber A B f y) = (is y).1 +-- rem2 (y:B) : fiber A B f y = (is y).2 +-- g (y:B) : A = (rem2 y).1 +-- s (y:B) : Id B y (f (g y)) = (rem2 y).2 +-- rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x) +-- rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = +-- rem1 (f x) (g (f x),rem3 x) (x,refl B (f x)) +-- t (x:A) : Id A (g (f x)) x = ((rem4 x)@i).1 -Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f - -lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g - = (h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i) - --- a general lemma about equivalence and fibrations - -Sigma (A:U) (F:A->U) : U = (x:A) * F x - -lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x) - (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : - isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2)) - where - AF : U = Sigma A F - AG : U = Sigma A G - g (xp : AF) : AG = (xp.1,f xp.1 xp.2) - rem1 : isContr (fiber AF AG g (x,v)) = h (x,v) - phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),(x,(z.2)@ i)) - psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport ( (u : F (p@-i)) * IdP (G (p@-i /\ j)) v (f (p@-i) u)) (w,q) - where yu : AF = z.1 - y : A = yu.1 - w : F y = yu.2 - p : Id A x y = (z.2 @ i).1 - q : IdP (G (p@j)) v (f y w) = ((z.2) @ i).2 - rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = psi ((rem1.1 (phi z0) (phi z1))@i) +-- Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f + +-- lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g +-- = (h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i) + +-- -- a general lemma about equivalence and fibrations + +-- Sigma (A:U) (F:A->U) : U = (x:A) * F x + +-- lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x) +-- (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : +-- isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2)) +-- where +-- AF : U = Sigma A F +-- AG : U = Sigma A G +-- g (xp : AF) : AG = (xp.1,f xp.1 xp.2) +-- rem1 : isContr (fiber AF AG g (x,v)) = h (x,v) +-- phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),(x,(z.2)@ i)) +-- psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport ( (u : F (p@-i)) * IdP (G (p@-i /\ j)) v (f (p@-i) u)) (w,q) +-- where yu : AF = z.1 +-- y : A = yu.1 +-- w : F y = yu.2 +-- p : Id A x y = (z.2 @ i).1 +-- q : IdP (G (p@j)) v (f y w) = ((z.2) @ i).2 +-- rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = psi ((rem1.1 (phi z0) (phi z1))@i) diff --git a/examples/gradLemma.ctt b/examples/gradLemma.ctt index 1c106d8..da89690 100644 --- a/examples/gradLemma.ctt +++ b/examples/gradLemma.ctt @@ -1,74 +1,126 @@ module gradLemma where -import prelude +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) - (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 ] - 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)) ] + (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) + (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = (fCenter,fIsCenter) + 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 + +-- Using gradLemma we get that any isomorphism gives a line in the universe +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 B [ (i = 0) -> (A,f,gradLemma A B f g s t) + , (i = 1) -> (B,transDelta B) ] + + + + +-- OLD CODE: +-- lemIso with equalities on other direction: -- 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) +-- 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) - (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)) +-- 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)) ] + +-- -- 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) +-- (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)) diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt index 81a71d9..816256d 100644 --- a/examples/hedberg.ctt +++ b/examples/hedberg.ctt @@ -2,28 +2,61 @@ module hedberg where import prelude -hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) : - (b : A) (p : Id A a b) -> - Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) = - J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p)) - (refl (Id A a a) (f a a (refl A a))) +hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) : + Square A a a a b (refl A a) p (f a (refl A a)) (f b p) = + comp ( Square A a a a (p @ i) (<_> a) ( p @ i /\ j) + (f a (<_> a)) (f (p @ i) ( p @ i /\ j))) + ( f a (<_> a)) [] -hedberg (A : U) (h : discrete A) : set A = \(a b : A) (p q : Id A a b) -> - let rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y) +hedbergStable (A : U) (a b : A) (h : (x : A) -> stable (Id A a x)) + (p q : Id A a b) : Id (Id A a b) p q = + comp (<_> A) a [ (j = 0) -> rem2 @ i + , (j = 1) -> rem3 @ i + , (i = 0) -> r + , (i = 1) -> rem4 @ j] + where + ra : Id A a a = <_> a + rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x) + f (x : A) : Id A a x -> Id A a x = (rem1 x).1 + fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2 + rem4 : Square A a a b b ra (refl A b) (f b p) (f b q) = fIsConst b p q + r : Id A a a = f a ra + rem2 : Square A a a a b ra p r (f b p) = hedbergLemma A a b f p + rem3 : Square A a a a b ra q r (f b q) = hedbergLemma A a b f q - f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1 +hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A = + \(a b : A) -> hedbergStable A a b (h a) - fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2 +hedberg (A : U) (h : discrete A) : set A = + \(a b : A) -> hedbergStable A a b (\(b : A) -> decStable (Id A a b) (h a b)) - r : Id A a a = f a a (refl A a) - rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p - rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q - rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q +-- Alternative version: - rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) = - compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q) - (f a b q) rem2 rem3 rem4 - in lemSimpl A a a b r p q rem5 +-- hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) : +-- (b : A) (p : Id A a b) -> +-- Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) = +-- J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p)) +-- (refl (Id A a a) (f a a (refl A a))) + +-- hedberg (A : U) (h : discrete A) : set A = \(a b : A) (p q : Id A a b) -> +-- let rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y) + +-- f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1 + +-- fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2 + +-- r : Id A a a = f a a (refl A a) + +-- rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p + +-- rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q + +-- rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q + +-- rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) = +-- compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q) +-- (f a b q) rem2 rem3 rem4 +-- in lemSimpl A a a b r p q rem5 diff --git a/examples/int.ctt b/examples/int.ctt index 3b9958e..f593479 100644 --- a/examples/int.ctt +++ b/examples/int.ctt @@ -2,6 +2,7 @@ module int where import nat import discor +import gradLemma -- inl = neg, inr = pos Z : U = or nat nat @@ -42,4 +43,4 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ -ZSet : set Z = corrhedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file +ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file diff --git a/examples/interval.ctt b/examples/interval.ctt index 50adb42..89a85da 100644 --- a/examples/interval.ctt +++ b/examples/interval.ctt @@ -1,6 +1,6 @@ module interval where -import prelude +import gradLemma data I = zero | one | seg [(i = 0) -> zero, (i = 1) -> one] diff --git a/examples/nat.ctt b/examples/nat.ctt index f084b83..5dd18d1 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -1,7 +1,6 @@ module nat where -import prelude -import newhedberg +import hedberg data nat = zero | suc (n : nat) @@ -16,6 +15,25 @@ add (m : nat) : nat -> nat = split zero -> m suc n -> suc (add m n) +add_zero : (n : nat) -> Id nat (add zero n) n = split + zero -> zero + suc n -> suc (add_zero n @ i) + +add_suc (a:nat) : (n : nat) -> Id nat (add (suc a) n) (suc (add a n)) = split + zero -> suc a + suc m -> suc (add_suc a m @ i) + +add_comm (a : nat) : (n : nat) -> Id nat (add a n) (add n a) = split + zero -> add_zero a @ -i + suc m -> comp (<_> nat) (suc (add_comm a m @ i)) + [ (i = 0) -> suc (add a m) + , (i = 1) -> add_suc m a @ -j ] + +assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = split + zero -> add a b + suc c1 -> suc (assocAdd a b c1@i) + + add' : nat -> nat -> nat = split zero -> \(x : nat) -> x suc n -> \(x : nat) -> suc (add' n x) @@ -54,6 +72,4 @@ natDec : (n m:nat) -> dec (Id nat n m) = split (\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> suc (p @ i)) (sucInj n m) (natDec n m)) --- natSet : set nat = hedberg nat natDec -natSet : set nat = corrhedberg nat natDec - +natSet : set nat = hedberg nat natDec diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt deleted file mode 100644 index 158660e..0000000 --- a/examples/newhedberg.ctt +++ /dev/null @@ -1,31 +0,0 @@ -module newhedberg where - -import prelude - -hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) : - Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = - comp ( Square A a a (<_> a) a (p @ i) ( p @ i /\ j) - (f a (<_> a)) (f (p @ i) ( p @ i /\ j))) - ( f a (<_> a)) [] - -hedberg (A : U) (a b : A) (h : (x : A) -> stable (Id A a x)) - (p q : Id A a b) : Id (Id A a b) p q = - comp (<_> A) a [ (j = 0) -> rem2 @ i - , (j = 1) -> rem3 @ i - , (i = 0) -> r - , (i = 1) -> rem4 @ j] - where - ra : Id A a a = <_> a - rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x) - f (x : A) : Id A a x -> Id A a x = (rem1 x).1 - fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2 - rem4 : Square A a a ra b b (refl A b) (f b p) (f b q) = fIsConst b p q - r : Id A a a = f a ra - rem2 : Square A a a ra a b p r (f b p) = hedbergLemma A a b f p - rem3 : Square A a a ra a b q r (f b q) = hedbergLemma A a b f q - -hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A = - \(a b : A) -> hedberg A a b (h a) - -corrhedberg (A : U) (h : discrete A) : set A = - \(a b : A) -> hedberg A a b (\(b : A) -> decStable (Id A a b) (h a b)) \ No newline at end of file diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 0fa5b97..ef39041 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -67,9 +67,9 @@ compDown (A : U) (a a' b b' : A) -- lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p = -- comp A (comp A (p @ i) [(i=1) -> q @ (-j /\ k)]) [(i=1) -> q @ (-j /\ - k)] --- lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) = --- comp A (p @ (-i \/ j)) [(i=1) -> p @ (j \/ k)] - +lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) = + comp (<_>A) (p @ (-i \/ j)) [(i=0) -> b, (j=1) -> b, (i=1) -> p @ (j \/ k)] + test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) @@ -97,35 +97,6 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) idfun (A : U) (a : A) : A = a --- 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) ] - --- 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 = 1) -> (B,g,f,t,s) --- , (i = 0) -> --- (A --- ,\ (x : A) -> comp (<_> A) x [ ] --- ,\ (y : A) -> comp (<_> A) y [ ] --- ,\ (y : A) -> comp (<_> A) (comp (<_> A) y [ ]) --- [ (i = 0) -> comp (<_> A) (comp (<_> A) y [ ]) --- [ (j = 0) -> <_> comp (<_> A) y [ ] ] --- , (i = 1) -> comp (<_> A) y [ (j = 1) -> <_> y ] --- ] --- ,\ (x : A) -> comp (<_> A) (comp (<_> A) x [ ]) --- [ (i = 0) -> comp (<_> A) (comp (<_> A) x [ ]) --- [ (j = 0) -> <_> comp (<_> A) x [ ] ] --- , (i = 1) -> comp (<_> A) x [ (j = 1) -> <_> x ] ]) --- ] - --- isoIdRef (A : U) : --- Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) = --- glueLine j i A - -- u -- a0 -----> a1 -- | | @@ -134,13 +105,12 @@ idfun (A : U) (a : A) : A = a -- V V -- b0 -----> b1 -- v - -Square (A : U) (a0 a1 : A) (u : Id A a0 a1) - (b0 b1 : A) (v : Id A b0 b1) +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 -constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p = +constSquare (A : U) (a : A) (p : Id A a a) : Square A a a a a p p p p = comp (<_>A) a [(i = 0) -> p @ (j \/ - k), (i = 1) -> p @ (j /\ k), @@ -163,24 +133,40 @@ propIsProp (A : U) (f g : prop A) : Id (prop A) f g = setIsProp (A : U) (f g : set A) : Id (set A) f g = \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i -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 - IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U = IdP ( P (p @ i)) u0 u1 +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 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 - --- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A) --- (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 = --- (pP (p @ i) (comp ( P (p @ i /\ j)) b0 [ ]) --- (comp ( P (p @ i \/ -j)) b1 [])) @ 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) + +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) -- Basic data types diff --git a/examples/retract.ctt b/examples/retract.ctt index 9c9c89f..7bfdbe6 100644 --- a/examples/retract.ctt +++ b/examples/retract.ctt @@ -17,18 +17,18 @@ retractInv (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y : A) (q: Id B (f x) (f y)) : Id A x y = compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y) ( (g (q @ i))) -lemRSquare (A B : U) (f : A -> B) (g : B -> A) (rfg: retract A B f g)(x y:A) (p : Id A x y) : - Square A (g (f x)) (g (f y)) ( g (f (p @ i))) x y - (retractInv A B f g rfg x y ( f (p@ i))) (rfg x) (rfg y) = - comp A (g (f (p @ j))) [(j=0) -> (rfg x) @ (i/\l), (j=1) -> (rfg y) @ (i/\l)] - -retractId (A B : U)(f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y :A) (p:Id A x y) : - Id (Id A x y) (retractInv A B f g rfg x y ( f (p@ i))) p = - comp A (g (f (p @ j))) [(j=0) -> rfg x,(j=1) -> rfg y, - (i=0) -> (lemRSquare A B f g rfg x y p) @ j,(i=1) -> rfg (p @ j)] - -retractSet (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) - (sB : set B) (x y : A) : prop (Id A x y) = - retractProp (Id A x y) (Id B (f x) (f y)) (mapOnPath A B f x y) - (retractInv A B f g rfg x y) (retractId A B f g rfg x y) (sB (f x) (f y)) +-- lemRSquare (A B : U) (f : A -> B) (g : B -> A) (rfg: retract A B f g)(x y:A) (p : Id A x y) : +-- Square A (g (f x)) (g (f y)) ( g (f (p @ i))) x y +-- (retractInv A B f g rfg x y ( f (p@ i))) (rfg x) (rfg y) = +-- comp A (g (f (p @ j))) [(j=0) -> (rfg x) @ (i/\l), (j=1) -> (rfg y) @ (i/\l)] + +-- retractId (A B : U)(f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y :A) (p:Id A x y) : +-- Id (Id A x y) (retractInv A B f g rfg x y ( f (p@ i))) p = +-- comp A (g (f (p @ j))) [(j=0) -> rfg x,(j=1) -> rfg y, +-- (i=0) -> (lemRSquare A B f g rfg x y p) @ j,(i=1) -> rfg (p @ j)] + +-- retractSet (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) +-- (sB : set B) (x y : A) : prop (Id A x y) = +-- retractProp (Id A x y) (Id B (f x) (f y)) (mapOnPath A B f x y) +-- (retractInv A B f g rfg x y) (retractId A B f g rfg x y) (sB (f x) (f y)) diff --git a/examples/univ.ctt b/examples/univ.ctt deleted file mode 100644 index 9a0e1b1..0000000 --- a/examples/univ.ctt +++ /dev/null @@ -1,379 +0,0 @@ -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 - --- Gradlemma: - --- 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 (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) - (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = (fCenter,fIsCenter) - 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 - - --- 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) - -univAx (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) (transEquivToId A B) - (idToId A B) (eqToEq A B) - - --- 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 diff --git a/examples/univalence.ctt b/examples/univalence.ctt index c6c5d5c..6512d28 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -1,18 +1,98 @@ module univalence where -import retract -import equiv +import gradLemma --- we do something simpler than univalence +transEquivToId (A B : U) (w : equiv A B) : Id U A B = + glue B [ (i=1) -> (B,transDelta B), (i=0) -> (A,w) ] -transpIsEquiv (A B:U) (p:Id U A B) : isEquiv A B (\ (x:A) -> transport p x) = - transport (isEquiv A (p@i) (\ (x:A) -> transport (p@i/\j) x)) (idIsEquiv A) +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,transDelta B) + , (j=1) -> (p@i,transEquiv (p@i) B ( p @ (i \/ k)))] -IdToEquiv (A B:U) (p: Id U A B) : Equiv A B = (\ (x:A) -> transport p x, transpIsEquiv A B p) +-- The normal form of this is much bigger than the normal form of eqToEq +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)]) -EquivToId (A B:U) (z:Equiv A B) : Id U A B = isEquivEq A B z.1 z.2 +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) -secIdEquiv (A B :U) (p : Id U A B) : Id (Id U A B) (EquivToId A B (IdToEquiv A B p)) p = - transport (Id (Id U A (p@i)) (EquivToId A (p@i) (IdToEquiv A (p@i) (p@i/\j))) (p@i/\j)) - (isoIdRef A@-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) + +univAx (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) (transEquivToId A B) + (idToId A B) (eqToEq A B) + + +-- Alternative definition: + +-- 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) ] + +idToEquivIdFun (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) + +idToEquivK (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 (idToEquivIdFun A B w) + +-- This takes too long to normalize: +test (A : U) : Id (equiv A A) (idToEquiv A A (equivToId A A (idEquiv A))) (idEquiv A) = + idToEquivK A A (idEquiv A) + + + + + + + +-- Old code: +-- -- we do something simpler than univalence + +-- transpIsEquiv (A B:U) (p:Id U A B) : isEquiv A B (\ (x:A) -> transport p x) = +-- transport (isEquiv A (p@i) (\ (x:A) -> transport (p@i/\j) x)) (idIsEquiv A) + +-- IdToEquiv (A B:U) (p: Id U A B) : Equiv A B = (\ (x:A) -> transport p x, transpIsEquiv A B p) + +-- EquivToId (A B:U) (z:Equiv A B) : Id U A B = isEquivEq A B z.1 z.2 + +-- secIdEquiv (A B :U) (p : Id U A B) : Id (Id U A B) (EquivToId A B (IdToEquiv A B p)) p = +-- transport (Id (Id U A (p@i)) (EquivToId A (p@i) (IdToEquiv A (p@i) (p@i/\j))) (p@i/\j)) +-- (isoIdRef A@-i)