From 612698ed862a19581a522330e95d28f58f6d9c89 Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 13 Apr 2015 15:53:07 +0200 Subject: [PATCH] Reorganized and cleaned some examples --- README.md | 6 ++-- examples/helix.ctt | 11 ------- examples/prelude.ctt | 5 +++ examples/uafunext.ctt | 45 -------------------------- examples/{funext.ctt => uafunext1.ctt} | 2 +- 5 files changed, 9 insertions(+), 60 deletions(-) delete mode 100644 examples/uafunext.ctt rename examples/{funext.ctt => uafunext1.ctt} (97%) diff --git a/README.md b/README.md index dd14e2f..0f15562 100644 --- a/README.md +++ b/README.md @@ -21,9 +21,9 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i ``` -This proof can be compared with the one in "examples/funext.ctt" which -proves that univalence implies function extensionality (the normal -form of these proofs are almost the same). +This proof can be compared with the one in "examples/uafunext1.ctt" +which proves that univalence implies function extensionality (the +normal form of these proofs are almost the same). For more examples, see "examples/demo.ctt". diff --git a/examples/helix.ctt b/examples/helix.ctt index 26988fb..4f5d750 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -73,12 +73,6 @@ lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = -- other proof? -propIsProp (A:U) (f g:prop A) : Id (prop A) f g = - \ (a b :A) -> (propSet A f a b (f a b) (g a b)) @ i - -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 - 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) @@ -89,11 +83,6 @@ setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix -- S1 is a groupoid -groupoid (A:U) : U = (x y:A) -> set (Id A x y) - -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 - isGroupoidS1 : groupoid S1 = lem where lem2 : (y : S1) -> set (Id S1 base y) diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 6e749f1..23d17e2 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -98,6 +98,7 @@ constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p = prop (A : U) : U = (a b : A) -> Id A a b set (A : U) : U = (a b : A) -> prop (Id A a b) +groupoid (A : U) : U = (a b : A) -> set (Id A a b) 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 @@ -111,6 +112,10 @@ 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 diff --git a/examples/uafunext.ctt b/examples/uafunext.ctt deleted file mode 100644 index 0c34054..0000000 --- a/examples/uafunext.ctt +++ /dev/null @@ -1,45 +0,0 @@ -module uafunext where - -import prelude - -diag (A : U) : U = (xy : ((_ : A) * A)) * (Id A xy.1 xy.2) - -pi1 (A : U) (d : diag A) : A = d.1.1 -pi2 (A : U) (d : diag A) : A = d.1.2 -toDiag (A : U) (a : A) : diag A = ((a,a),refl A a) - -toDiagK1 (A : U) : (x : diag A) -> Id (diag A) (toDiag A (pi1 A x)) x = undefined -pi1K (A : U) : (x : A) -> Id A (pi1 A (toDiag A x)) x = undefined - --- toDiagK2 (A : U) : (x : diag A) -> Id (diag A) (toDiag A (pi2 A x)) x = undefined --- pi2K (A : U) : (x : A) -> Id A (pi2 A (toDiag A x)) x = undefined - --- elimIso (A : U) (P : (B : U) -> (A -> B) -> (B -> A) -> U) --- (p : P A (idfun A) (idfun 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) : P B f g = undefined - -lem (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) - (C : U) (d e : C -> A) - (p : Id (C -> B) (\(x : C) -> f (d x)) (\(x : C) -> f (e x))) - : Id (C -> A) d e = undefined - -uaFunExt (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) : - Id (A -> B) f g = suff - where - d (a : A) : diag B = ((f a,f a),refl B (f a)) - e (a : A) : diag B = ((f a,g a),p a) - - -- By eta it suffices to prove: - suff : Id (A -> B) (\(x : A) -> pi2 B (d x)) (\(x : A) -> pi2 B (e x)) = - subst (A -> diag B) - (\(f : A -> diag B) -> Id (A -> B) (\(x : A) -> pi2 B (d x)) (\(x : A) -> pi2 B (f x))) - d e eq_de ( \(x : A) -> pi2 B (d x)) - where - -- This is the key fact: - eq_de : Id (A -> diag B) d e = - lem (diag B) B (pi1 B) (toDiag B) (pi1K B) (toDiagK1 B) A d e ( \(x : A) -> f x) - diff --git a/examples/funext.ctt b/examples/uafunext1.ctt similarity index 97% rename from examples/funext.ctt rename to examples/uafunext1.ctt index 60e50f5..fbf840c 100644 --- a/examples/funext.ctt +++ b/examples/uafunext1.ctt @@ -1,4 +1,4 @@ -module funext where +module uafunext1 where import prelude -- 2.34.1