From 612698ed862a19581a522330e95d28f58f6d9c89 Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
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 = <i> \(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 =
- <i> \ (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 =
- <i> \ (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 
-  = <i> \ (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 =
  <j i> 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 =
  <i> \(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 
+  = <i> \ (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 (<i> 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 (<i> \(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 (<i> \(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