From 48e391324358a820b9e5222a0945b3bc6f6aa63c Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Wed, 8 Apr 2015 10:21:02 +0200 Subject: [PATCH] added thierrys adapted files --- examples/discor.ctt | 64 ++++++++++++++++++++++++ examples/hedberg.ctt | 88 +++++++++++++++++++++++++++++++++ examples/int.ctt | 42 ++++++++++++++++ examples/retract.ctt | 36 ++++++++++++++ examples/susp.ctt | 114 +++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 344 insertions(+) create mode 100644 examples/discor.ctt create mode 100644 examples/hedberg.ctt create mode 100644 examples/int.ctt create mode 100644 examples/retract.ctt create mode 100644 examples/susp.ctt diff --git a/examples/discor.ctt b/examples/discor.ctt new file mode 100644 index 0000000..ecfc665 --- /dev/null +++ b/examples/discor.ctt @@ -0,0 +1,64 @@ +module discor where + +import prelude + +data or (A B:U) = inl (a:A) | inr (b:B) + +data Unit = tt + +data N0 = + +efq (A:U) : N0 -> A = split{} + +neg (A:U) : U = A -> N0 + +dec (A:U) : U = or A (neg A) + +discrete (A:U) : U = (a b:A) -> dec (Id A a b) + +inlNotinr (A B:U) (a:A) (b:B) (h: Id (or A B) (inl a) (inr b)) : N0 = + subst (or A B) T (inl a) (inr b) h tt + where + T : or A B -> U = split + inl _ -> Unit + inr _ -> N0 + +inrNotinl (A B:U) (a:A) (b:B) (h : Id (or A B) (inr b) (inl a)) : N0 = + subst (or A B) T (inr b) (inl a) h tt + where + T : or A B -> U = split + inl _ -> N0 + inr _ -> Unit + +injective (A B:U) (f:A->B) : U = (a0 a1:A) -> Id B (f a0) (f a1) -> Id A a0 a1 + +injInl (A B :U) (x0 x1:A) (h : Id (or A B) (inl x0) (inl x1)) : Id A x0 x1 = + subst (or A B) T (inl x0) (inl x1) h (refl A x0) + where + T : or A B -> U = split + inl x -> Id A x0 x + inr _ -> N0 + +injInr (A B :U) (x0 x1:B) (h: Id (or A B) (inr x0) (inr x1)) : Id B x0 x1 = + subst (or A B) T (inr x0) (inr x1) h (refl B x0) + where + T : or A B -> U = split + inl _ -> N0 + inr x -> Id B x0 x + +orDisc (A B : U) (dA: discrete A) (dB: discrete B) : (z z1 : or A B) -> dec (Id (or A B) z z1) = split + inl a -> rem1 + where rem1 : (z1:or A B) -> dec (Id (or A B) (inl a) z1) = split + inl a1 -> rem (dA a a1) + where rem : dec (Id A a a1) -> dec (Id (or A B) (inl a) (inl a1)) = split + inl p -> inl ( inl (p @ i)) + inr h -> inr (\ (p:Id (or A B) (inl a) (inl a1)) -> h (injInl A B a a1 p)) + inr b -> inr (inlNotinr A B a b) + inr b -> rem1 + where rem1 : (z1:or A B) -> dec (Id (or A B) (inr b) z1) = split + inl a -> inr (inrNotinl A B a b) + inr b1 -> rem (dB b b1) + where rem : dec (Id B b b1) -> dec (Id (or A B) (inr b) (inr b1)) = split + inl p -> inl ( inr (p @ i)) + inr h -> inr (\ (p:Id (or A B) (inr b) (inr b1)) -> h (injInr A B b b1 p)) + diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt new file mode 100644 index 0000000..a9443f3 --- /dev/null +++ b/examples/hedberg.ctt @@ -0,0 +1,88 @@ +module hedberg where + +import bool +import discor +import int + +const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y) + +decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split + inl a -> inl (f a) + inr h -> inr (\ (b:B) -> h (g b)) + +pred : nat -> nat = split + zero -> zero + suc n -> n + +sucInj (n m : nat) (p:Id nat (suc n) (suc m)) : Id nat n m = + pred (p @ i) + +caseNat (A:U) (a0 aS : A) : nat -> A = split + zero -> a0 + suc n -> aS + +caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) + : (n:nat) -> P n = split + zero -> a0 + suc n -> aS n + +znots (n : nat) : neg (Id nat zero (suc n)) = + \ (h:Id nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero + +snotz (n : nat) : neg (Id nat (suc n) zero) = + \ (h:Id nat (suc n) zero) -> znots n (inv nat (suc n) zero h) + +natDec : (n m:nat) -> dec (Id nat n m) = split + zero -> caseDNat (\ (m:nat) -> dec (Id nat zero m)) (inl (refl nat zero)) (\ (m:nat) -> inr (znots m)) + suc n -> caseDNat (\ (m:nat) -> dec (Id nat (suc n) m)) (inr (snotz n)) + (\ (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)) + +prop (A:U) : U = (a b:A) -> Id A a b + +set (A:U) : U = (a b:A) -> prop (Id A a b) + +exConst (A : U) :U = (f:A -> A) * const A f + +decConst (A : U) : dec A -> exConst A = split + inl a -> (\ (x:A) -> a, \ (x y:A) -> refl A a) + inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x)) + +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))) + +compUp (A : U) (a a' b b' : A) + (p : Id A a a') (q: Id A b b') (r:Id A a b) : Id A a' b' = + comp A (r@i) [(i=0) -> p, (i=1) -> q] + +compDown (A : U) (a a' b b' : A) + (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b = + compUp A a' a b' b (inv A a a' p) (inv A b b' q) + +hedberg (A : U) (h:discrete A) (a b :A) (p q:Id A a b) : Id (Id A a b) p q = + lemSimpl A a a b r p q rem5 + where + 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 + +natSet : set nat = hedberg nat natDec + +ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file diff --git a/examples/int.ctt b/examples/int.ctt new file mode 100644 index 0000000..3ff9691 --- /dev/null +++ b/examples/int.ctt @@ -0,0 +1,42 @@ +module int where + +import nat +import discor + +Z : U = or nat nat + +zeroZ : Z = inr zero + +sucZ : Z -> Z = split + inl u -> auxsucZ u + where + auxsucZ : nat -> Z = split + zero -> inr zero + suc n -> inl n + inr v -> inr (suc v) + +predZ : Z -> Z = split + inl u -> inl (suc u) + inr v -> auxpredZ v + where + auxpredZ : nat -> Z = split + zero -> inl zero + suc n -> inr n + +sucpredZ : (x : Z) -> Id Z (sucZ (predZ x)) x = split + inl u -> refl Z (inl u) + inr v -> lem v + where + lem : (u : nat) -> Id Z (sucZ (predZ (inr u))) (inr u) = split + zero -> refl Z (inr zero) + suc n -> refl Z (inr (suc n)) + +predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split + inl u -> lem u + where + lem : (u : nat) -> Id Z (predZ (sucZ (inl u))) (inl u) = split + zero -> refl Z (inl zero) + suc n -> refl Z (inl (suc n)) + inr v -> refl Z (inr v) + +sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ diff --git a/examples/retract.ctt b/examples/retract.ctt new file mode 100644 index 0000000..66a0bb8 --- /dev/null +++ b/examples/retract.ctt @@ -0,0 +1,36 @@ +module retract where + +import prelude +import hedberg + + +section (A B : U) (f : A -> B) (g : B -> A) :U = (b : B) -> Id B (f (g b)) b + +retract (A B : U) (f : A -> B) (g : B -> A) : U = section B A g f + +lemRetract (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y:A) : + Id A (g (f x)) (g (f y)) -> Id A x y + = compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y) + +retractProp (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (pB :prop B) (x y:A) + : Id A x y = lemRetract A B f g rfg x y ( g (pB (f x) (f y)) @ i) + +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)) + diff --git a/examples/susp.ctt b/examples/susp.ctt new file mode 100644 index 0000000..905cbc9 --- /dev/null +++ b/examples/susp.ctt @@ -0,0 +1,114 @@ +module susp where + +-- import helix +import circle + +data susp (A:U) = north | south | merid (a:A) @ north ~ south + +-- n-spheres +sphere : nat -> U = split + zero -> bool + suc n -> susp (sphere n) + +-- The circle (S1) is equal to the 1-sphere (aka the suspension of Bool). +-- (Similar to HoTT Book, Lemma 6.5.1) +one : nat = suc zero + +sone : U = sphere one + +s1ToCircle : sone -> S1 = split + north -> base + south -> base + merid b @ i -> (path b) @ i + where path : bool ->Id S1 base base = split + false -> loop' + true -> refl S1 base + +m0 : Id sone north south = (merid{sone} false) @ i + +m1 : Id sone north south = (merid{sone} true) @ i + +invm1 : Id sone south north = inv sone north south m1 + +circleToS1 : S1 -> sone = split + base -> north + loop @ i -> (compId sone north south north m0 invm1) @ i + +merid1 (b:bool) : Id sone north south = (merid{sone} b)@ i + +oc (x:S1) : S1 = s1ToCircle (circleToS1 x) + +ocid : (x : S1) -> Id S1 (oc x) x = split + base -> refl S1 base + loop @ i -> oc (loop' @ i) + +co (x: sone) : sone = circleToS1 (s1ToCircle x) + +lemSquare (A:U) (a b : A) (m0 m1 : Id A a b) : + Square A a a (compId A a b a m0 (inv A a b m1)) a b m0 (refl A a) m1 = + comp A (m0 @ j) [(j=1) -> m1 @ (i \/ -k) + ,(i=0) -> comp A (m0 @ j) [(j=1) -> m1 @ (-k \/ -l)]] + +coid : (x : sone) -> Id sone (co x) x = split + north -> refl sone north + south -> m1 + merid b @ i -> (ind b) @ i + where + F (x:sone) : U = Id sone (co x) x + + ind : (b:bool) -> IdS sone F north south (merid1 b) (refl sone north) m1 = split + false -> lemSquare sone north south m0 m1 + true -> m1 @ (j /\ k) + +s1EqCircle : Id U sone S1 = isoId sone S1 s1ToCircle circleToS1 ocid coid + +s1EqS1 : Id U S1 S1 = compId U S1 sone S1 (inv U sone S1 s1EqCircle) s1EqCircle + +-- pointed sets + +ptU : U = (X : U) * X + +lemPt1 (A :U) : (B:U) (p:Id U A B) (a:A) -> Id ptU (A,a) (B,transport p a) + = J U A (\ (B:U) (p:Id U A B) -> (a:A) -> Id ptU (A,a) (B,transport p a)) + (\ (a:A) -> refl ptU (A,a)) + +s1PtCircle1 : Id ptU (sone,north) (S1,base) = lemPt1 sone S1 s1EqCircle north + +lemPt (A :U) (B:U) (p:Id U A B) (a:A) : Id ptU (A,a) (B,transport p a) = + (p @ i,transport (p @ (i/\j)) a) + +Omega (X:ptU) : ptU = (Id X.1 X.2 X.2,refl X.1 X.2) + +s1PtCircle : Id ptU (sone,north) (S1,base) = lemPt sone S1 s1EqCircle north + +s1PtS1 : Id ptU (S1,base) (S1,base) = lemPt S1 S1 s1EqS1 base + +windingS : Id sone north north -> Z = rem1 + where + G (X:ptU) : U = (Omega X).1 -> Z + rem : G (S1,base) = winding + rem1 : G (sone,north) = subst ptU G (S1,base) (sone,north) ( s1PtCircle @ -i) rem + +windingT : loopS1 -> Z = rem1 + where + G (X: ptU): U = (Omega X).1 -> Z + rem : G (S1,base) = winding + rem1 : G (S1,base) = subst ptU G (S1,base) (S1,base) s1PtS1 rem + +s1ToCId (p: Id sone north north) : Id S1 base base + = transport s1EqCircle (p @ i) + +s1ToCIdInv (p : Id S1 base base) : Id sone north north + = (transport ( s1EqCircle @(-j)) (p @ i)) + +loop1S : Id sone north north = s1ToCIdInv loop' + +loop2S : Id sone north north = compId sone north north north loop1S loop1S + +test0S : Z = windingS (refl sone north) + +test2S : Z = windingS loop2S + +winding' (l : Id sone north north) : Z = winding (s1ToCId l) + +testS : Id sone north north = comp sone (m0 @ i) [ (i=1) -> m1 @ (-k)] -- 2.34.1