new proof of Hedberg's theorem

diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
new file mode 100644 (file)
index 0000000..02e9bac
--- /dev/null
+++ b/examples/newhedberg.ctt
@@ -0,0 +1,35 @@
+module newhedberg where\r
+\r
+import prelude\r
+\r
+const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)\r
+\r
+decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split\r
+  inl a -> inl (f a)\r
+  inr h -> inr (\ (b:B) -> h (g b))\r
+\r
+exConst (A : U) : U = (f:A -> A) * const A f\r
+\r
+decConst (A : U) : dec A -> exConst A = split\r
+  inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)\r
+  inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x))\r
+\r
+hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :\r
+            Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = \r
+ transport (<i>Square A a a (refl A a) a p@i (<j>p@i/\j) (f a (refl A a)) (f p@i (<j>p@i/\j)))\r
+    (<i>(f a (refl A a)))\r
+\r
+hedberg (A:U) (a b:A) (h: (x:A) -> dec (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q =\r
+ <j i>comp A a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j]\r
+ where \r
+   ra : Id A a a = refl A a \r
+   rem1 (x:A) : exConst (Id A a x) = decConst (Id A a x) (h x)\r
+   f (x:A) : Id A a x -> Id A a x  = (rem1 x).1\r
+   fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2\r
+   rem4 : Square A a a ra b b (refl A b) (f b p) (f b q)  = fIsConst b p q\r
+   r : Id A a a = f a ra\r
+   rem2 : Square A a a ra a b p r (f b p) = hedbergLemma A a b f p\r
+   rem3 : Square A a a ra a b q r (f b q) = hedbergLemma A a b f q\r
+\r
+corrhedberg (A:U) (h : discrete A) : set A =\r
+ \ (a b :A) -> hedberg A a b (h a)
\ No newline at end of file