From 4ccf678a4ede6c4d307738faac7b17b26eb319cc Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 13 Apr 2015 16:39:28 +0200 Subject: [PATCH] Lots of cleaning in the examples --- examples/bool.ctt | 20 +++++++-------- examples/circle.ctt | 29 ++++++++++++--------- examples/discor.ctt | 20 +++------------ examples/equiv.ctt | 2 -- examples/hedberg.ctt | 60 ++++++++++++------------------------------- examples/helix.ctt | 23 ----------------- examples/int.ctt | 2 ++ examples/interval.ctt | 1 + examples/nat.ctt | 25 +++++++++++++++++- examples/prelude.ctt | 39 +++++++++++++++++++++++++--- examples/susp.ctt | 10 +++++--- 11 files changed, 115 insertions(+), 116 deletions(-) diff --git a/examples/bool.ctt b/examples/bool.ctt index dbbcab8..f94af65 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -4,18 +4,18 @@ import prelude data bool = false | true -neg : bool -> bool = split +negBool : bool -> bool = split false -> true true -> false -negK : (b : bool) -> Id bool (neg (neg b)) b = split +negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split false -> refl bool false true -> refl bool true -negEq : Id U bool bool = - glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ] +negBoolEq : Id U bool bool = + glue bool [ (i = 0) -> (bool,negBool,negBool,negBoolK,negBoolK) ] -test : bool = transport negEq true +test : bool = transport negBoolEq true data F2 = zeroF2 | oneF2 @@ -38,7 +38,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split boolEqF2 : Id U bool F2 = isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K -negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg +negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A) @@ -48,21 +48,21 @@ test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2 -negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2 +negBool' : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2 F2EqBoolComp : Id U F2 bool = - compId U F2 bool bool F2EqBool negEq + compId U F2 bool bool F2EqBool negBoolEq test2 : bool = transport F2EqBoolComp oneF2 negNegEq : Id U bool bool = - compId U bool bool bool negEq negEq + compId U bool bool bool negBoolEq negBoolEq test3 : bool = transport negNegEq true test4 : Id U bool bool = negNegEq @ i kanBool : Id U bool bool = - kan U bool bool bool bool negEq negEq negEq + kan U bool bool bool bool negBoolEq negBoolEq negBoolEq squareBoolF2 : Square U bool bool (refl U bool) bool F2 boolEqF2 (refl U bool) boolEqF2 = diff --git a/examples/circle.ctt b/examples/circle.ctt index d7a0a17..758e412 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -1,34 +1,39 @@ module circle where import bool -import integer +import int -data S1 = base | loop @ base ~ base +data S1 = base + | loop @ base ~ base + +loopS1 : U = Id S1 base base + +loop1 : Id S1 base base = loop{S1} @ i + +invLoop : loopS1 = inv S1 base base loop1 moebius : S1 -> U = split base -> bool - loop @ i -> negEq @ i - -loop' : Id S1 base base = loop{S1} @ i + loop @ i -> negBoolEq @ i helix : S1 -> U = split base -> Z loop @ i -> sucIdZ @ i -loopS1 : U = Id S1 base base - winding (p : loopS1) : Z = transport rem zeroZ where rem : Id U Z Z = helix (p @ i) +compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base + -- All of these should be equal to "posZ (suc zero)": -loop2 : loopS1 = compId S1 base base base loop' loop' -loop2' : loopS1 = compId' S1 base base base loop' loop' -loop2'' : loopS1 = compId'' S1 base base loop' base loop' +loop2 : loopS1 = compS1 loop1 loop1 +loop2' : loopS1 = compId' S1 base base base loop1 loop1 +loop2'' : loopS1 = compId'' S1 base base loop1 base loop1 mLoop : (x : S1) -> Id S1 x x = split - base -> loop' - loop @ i -> (constSquare S1 base loop') @ i + base -> loop1 + loop @ i -> (constSquare S1 base loop1) @ i mult (x : S1) : S1 -> S1 = split base -> x diff --git a/examples/discor.ctt b/examples/discor.ctt index ecfc665..e983ff1 100644 --- a/examples/discor.ctt +++ b/examples/discor.ctt @@ -2,20 +2,6 @@ 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 @@ -30,8 +16,6 @@ inrNotinl (A B:U) (a:A) (b:B) (h : Id (or A B) (inr b) (inl a)) : N0 = 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 @@ -46,7 +30,9 @@ injInr (A B :U) (x0 x1:B) (h: Id (or A B) (inr x0) (inr x1)) : Id B x0 x1 = 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 +-- If A and B are discrete then "A or B" is discrete +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) diff --git a/examples/equiv.ctt b/examples/equiv.ctt index 5e32517..d1d860a 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -2,8 +2,6 @@ module equiv where import prelude -and (A B:U) :U = (_:A) * B - contr (A:U) : U = (_:A) * prop A isContr (A : U) : U = and (prop A) A diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt index e1a60c6..9db5b1d 100644 --- a/examples/hedberg.ctt +++ b/examples/hedberg.ctt @@ -1,8 +1,6 @@ module hedberg where -import bool -import discor -import int +import prelude const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y) @@ -10,60 +8,34 @@ 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)) -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)) - 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) : +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)) + 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) (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 +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) - r : Id A a a = f a a (refl A a) + f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1 - rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p + fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2 - rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q + r : Id A a a = f a a (refl A a) - rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q + rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p - 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 + rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q -natSet : set nat = hedberg nat natDec + rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q -ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file + 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/helix.ctt b/examples/helix.ctt index 4f5d750..df89a0b 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -4,19 +4,12 @@ import circle import hedberg import retract -loop1 : loopS1 = loop' -triv : loopS1 = base - -compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base - encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ itLoop : nat -> loopS1 = split zero -> triv suc n -> compS1 (itLoop n) loop1 -invLoop : loopS1 = inv S1 base base loop1 - itLoopNeg : nat -> loopS1 = split zero -> invLoop suc n -> compS1 (itLoopNeg n) invLoop @@ -28,12 +21,6 @@ loopIt : Z -> loopS1 = split lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (Id S1 base (loop{S1} @ i)) (itLoop n)) = refl loopS1 (itLoop (suc n)) -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)] - lemItNeg : (n:nat) -> Id loopS1 (transport (Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split zero -> lemInv S1 base base loop1 suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop @@ -71,8 +58,6 @@ lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = base -> bP loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i --- other proof? - helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x) @@ -82,7 +67,6 @@ retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet -- S1 is a groupoid - isGroupoidS1 : groupoid S1 = lem where lem2 : (y : S1) -> set (Id S1 base y) @@ -182,10 +166,3 @@ invLaw : (x y : S1) -> (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) bP : P base base = refl (Id S1 base base) (refl S1 base) - - --- homotopy - -aLoop : loopS1 = loop{S1}@(i/\-i) - -test : Id loopS1 triv aLoop = loop{S1}@(j/\i/\-i) diff --git a/examples/int.ctt b/examples/int.ctt index 3ff9691..3d12f32 100644 --- a/examples/int.ctt +++ b/examples/int.ctt @@ -40,3 +40,5 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split inr v -> refl Z (inr v) sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ + +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 ee1f108..d5a2c43 100644 --- a/examples/interval.ctt +++ b/examples/interval.ctt @@ -4,6 +4,7 @@ import prelude data I = zero | one | seg @ zero ~ one +-- Proof of funext from the interval fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) : Id (A -> B) f g = (\(x : A) -> htpy x (seg{I} @ j)) where htpy (x : A) : I -> B = split diff --git a/examples/nat.ctt b/examples/nat.ctt index a3a7be4..f36e78d 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -1,6 +1,6 @@ module nat where -import prelude +import hedberg data nat = zero | suc (n : nat) @@ -31,3 +31,26 @@ test : Id (nat -> nat) idnat (idfun nat) = funExt nat (\(_ : nat) -> nat) idnat rem : (n : nat) -> Id nat (idnat n) n = split zero -> refl nat zero suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n) + +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)) + +natSet : set nat = hedberg nat natDec diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 23d17e2..c584fe6 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -1,5 +1,7 @@ module prelude where +-- Identity types + Id (A : U) (a0 a1 : A) : U = IdP ( A) a0 a1 refl (A : U) (a : A) : Id A a a = a @@ -18,6 +20,9 @@ subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = substRefl (A : U) (P : A -> U) (a : A) (e : P a) : Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e +substInv (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P b -> P a = + subst A P b a ( p @ -i) + singl (A : U) (a : A) : U = (x : A) * Id A a x contrSingl (A : U) (a b : A) (p : Id A a b) : @@ -51,7 +56,11 @@ 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) -idfun (A : U) (a : A) : A = 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)] 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) @@ -113,7 +122,7 @@ 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 + (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 = @@ -122,4 +131,28 @@ IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : 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) (transport ( P (p @ i /\ j)) b0) - (transport ( P (p @ i \/ -j)) b1)) @ i \ No newline at end of file + (transport ( P (p @ i \/ -j)) b1)) @ i + + +-- Basic data types + +data N0 = + +efq (A : U) : N0 -> A = split{} +neg (A : U) : U = A -> N0 + +data Unit = tt + +data or (A B : U) = inl (a : A) + | inr (b : B) + +dec (A : U) : U = or A (neg A) + +discrete (A : U) : U = (a b : A) -> dec (Id A a b) + +injective (A B : U) (f : A -> B) : U = + (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1 + +idfun (A : U) (a : A) : A = a + +and (A B : U) : U = (_ : A) * B diff --git a/examples/susp.ctt b/examples/susp.ctt index 161141d..c1212ce 100644 --- a/examples/susp.ctt +++ b/examples/susp.ctt @@ -2,7 +2,9 @@ module susp where import circle -data susp (A:U) = north | south | merid (a:A) @ north ~ south +data susp (A : U) = north + | south + | merid (a:A) @ north ~ south -- n-spheres sphere : nat -> U = split @@ -18,7 +20,7 @@ s1ToCircle : sone -> S1 = split south -> base merid b @ i -> (path b) @ i where path : bool ->Id S1 base base = split - false -> loop' + false -> loop1 true -> refl S1 base m0 : Id sone north south = (merid{sone} false) @ i @@ -37,7 +39,7 @@ 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) + loop @ i -> oc (loop1 @ i) co (x: sone) : sone = circleToS1 (s1ToCircle x) @@ -98,7 +100,7 @@ s1ToCId (p: Id sone north north) : Id S1 base base s1ToCIdInv (p : Id S1 base base) : Id sone north north = (transport ( s1EqCircle @(-j)) (p @ i)) -loop1S : Id sone north north = s1ToCIdInv loop' +loop1S : Id sone north north = s1ToCIdInv loop1 loop2S : Id sone north north = compId sone north north north loop1S loop1S -- 2.34.1