Start the proof that ua implies funext

diff --git a/examples/uafunext.ctt b/examples/uafunext.ctt
new file mode 100644 (file)
index 0000000..0c34054
--- /dev/null
+++ b/examples/uafunext.ctt
@@ -0,0 +1,45 @@
+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)
+