From: coquand <coquand@chalmers.se>
Date: Tue, 21 Apr 2015 14:57:12 +0000 (+0200)
Subject: updated proofs of Hedberg's Theorem
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=cde2f940f123bedcb5b461691b08a676e2a04875;p=cubicaltt.git

updated proofs of Hedberg's Theorem
---

diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt
index ca180af..f0f760b 100644
--- a/examples/newhedberg.ctt
+++ b/examples/newhedberg.ctt
@@ -10,20 +10,19 @@ decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split
 
 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))
+stableConst (A : U) (sA: stable A) : exConst A = 
+ (\ (x:A) -> sA (dNeg A x),\ (x y:A) -> <i>sA (propNeg (neg A) (dNeg A x) (dNeg A y) @ i))
 
 hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) :
             Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = 
  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)))
     (<i>(f a (refl A a)))
 
-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 =
+hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q =
  <j i>comp A a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j]
  where 
    ra : Id A a a = refl A a 
-   rem1 (x:A) : exConst (Id A a x) = decConst (Id A a x) (h x)
+   rem1 (x:A) : exConst (Id A a x) = stableConst (Id A a x) (h x)
    f (x:A) : Id A a x -> Id A a x  = (rem1 x).1
    fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2
    rem4 : Square A a a ra b b (refl A b) (f b p) (f b q)  = fIsConst b p q
@@ -31,5 +30,16 @@ hedberg (A:U) (a b:A) (h: (x:A) -> dec (Id A a x)) (p q : Id A a b) : Id (Id A a
    rem2 : Square A a a ra a b p r (f b p) = hedbergLemma A a b f p
    rem3 : Square A a a ra a b q r (f b q) = hedbergLemma A a b f q
 
+hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A =
+ \ (a b:A) -> hedberg A a b (h a)
+
+{- normal form
+ \(A : U) -> 
+ \(h : (a x : A) -> (((IdP (<!0> A) a x) -> N0) -> N0) -> (IdP (<!0> A) a x)) -> 
+ \(a b : A) -> 
+ \(p q : IdP (<!0> A) a b) ->
+ <!0 !1> comp A a [ (!0 = 0) -> <!2> comp A (comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !2) [ (!2 = 1) -> <!3> p @ (!3 /\ !1) ]) [ (!1 = 1) -> <!3> comp A (h a (p @ !3) (\(h0 : (IdP (<!1> A) a (p @ !3)) -> N0) -> h0 (<!1> p @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> <!4> p @ (!3 \/ !4) ] ], (!0 = 1) -> <!2> comp A (comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !2) [ (!2 = 1) -> <!3> q @ (!3 /\ !1) ]) [ (!1 = 1) -> <!3> comp A (h a (q @ !3) (\(h0 : (IdP (<!1> A) a (q @ !3)) -> N0) -> h0 (<!1> q @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> <!4> q @ (!3 \/ !4) ] ], (!1 = 0) -> <!2> h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !2, (!1 = 1) -> <!2> h a b (\(x : (IdP (<!0> A) a b) -> N0) -> efq (IdP (<!0> N0) (x p) (x q)) (x p) @ !0) @ !2 ]
+-}
+
 corrhedberg (A:U) (h : discrete A) : set A =
- \ (a b :A) -> hedberg A a b (h a)
\ No newline at end of file
+ \ (a b :A) -> hedberg A a b (\ (b:A) -> decStable (Id A a b) (h a b))
\ No newline at end of file
diff --git a/examples/other.ctt b/examples/other.ctt
new file mode 100644
index 0000000..f90c3fe
--- /dev/null
+++ b/examples/other.ctt
@@ -0,0 +1,62 @@
+module other where
+
+import retract
+
+propUnit : prop Unit = rem
+ where rem1 : (x:Unit) -> Id Unit x tt = split tt -> refl Unit tt
+       rem (x:Unit) : (y:Unit) -> Id Unit x y = split tt -> rem1 x
+
+setUnit : set Unit = propSet Unit propUnit
+
+propSingl (A:U) (a:A) (u v : singl A a) : Id (singl A a) u v =
+ compId (singl A a) u (a,refl A a) v (<i>(contrSingl A a u.1 u.2)@-i) (contrSingl A a v.1 v.2)
+
+singlN (A:U) (a:A) : U = (x:A) * neg (neg (Id A a x))
+
+injN (A:U) (a:A) : singlN A a = (a,\ (h:neg (Id A a a)) -> h (refl A a))
+
+lem1 (A:U) (a:A) (h:(x:A) -> stable (Id A a x)) : prop (singlN A a) = 
+ retractProp T (singl A a) f g rfg (propSingl A a)
+ where
+  T :U = (x:A) * neg (neg (Id A a x))
+  f (u:T) : singl A a = (u.1,h u.1 u.2)
+  g (u:singl A a) : T = (u.1,\ (z:neg (Id A a u.1)) -> z u.2)
+  rfg (u:T) : Id T (g (f u)) u = <i>(u.1,(propNeg (neg (Id A a u.1)) (g (f u)).2 u.2)@i)
+ 
+cor1 (A:U) (a:A) (h:(x:A) -> stable (Id A a x)) : set (singlN A a) = 
+ propSet (singlN A a) (lem1 A a h)
+
+lem2 (A:U) (a:A) (h:(x:A) -> stable (Id A a x)) : prop (Id A a a) = 
+ retractProp (Id A a a) B f g rfg (cor1 A a h ia ia)
+ where
+ ia : singlN A a = injN A a 
+ B : U = Id (singlN A a) ia ia
+ P (x:A) : U = neg (neg (Id A a x))
+ pP (x:A) : prop (P x) = propNeg (neg (Id A a x))
+ na : P a = \ (h:neg (Id A a a)) -> h (refl A a)
+ f (p:Id A a a) : B = <i>(p@i,(lemPropF A P pP a a p na na)@i)
+ g (p:B) : Id A a a = <i>(p@i).1
+ rfg (p:Id A a a) : Id (Id A a a) (g (f p)) p = refl (Id A a a) p
+
+lem3 (A:U) (h : (a:A) -> prop (Id A a a)) (a b:A) (p q : Id A a b) : Id (Id A a b) p q =
+ transport (<i>prop (Id A a (p@i))) (h a) p q
+
+{-
+ \(A : U) -> 
+ \(h : (a : A) -> (a0 : IdP (<i> A) a a) -> (b : IdP (<i> A) a a) -> IdP (<i> IdP (<i> A) a a) a0 b) -> 
+ \(a : A) -> 
+ \(b : A) -> 
+ \(p : IdP (<i> A) a b) -> \(q : IdP (<i> A) a b) -> 
+ <j> <k> comp A (comp A (h a (<j> comp A (p @ j) [ (j = 1) -> <i> p @ -i ]) (<j> comp A (q @ j) [ (j = 1) -> <i> p @ -i ]) @ j @ k) [ (k = 1) -> <i> p @ i ]) [ (j = 0) -> <i> comp A (comp A (p @ k) [ (k = 1) -> <j> p @ (i \/ -j) ]) [ (k = 1) -> <j> p @ (i \/ j) ], (j = 1) -> <i> comp A (comp A (q @ k) [ (k = 1) -> <j> p @ (i \/ -j) ]) [ (k = 1) -> <j> p @ (i \/ j) ] ]
+-}
+
+hedberg (A:U) (h : (a x:A) -> stable (Id A a x)) : set A =
+ lem3 A (\ (a:A) -> lem2 A a (h a))
+
+{- normal form
+ \(A : U) ->
+ \(h : (a x : A) -> (((IdP (<!0> A) a x) -> N0) -> N0) -> (IdP (<!0> A) a x)) ->
+ \(a b : A) ->
+ \(p q : IdP (<!0> A) a b) -> 
+ <!1 !2> comp A (comp A (comp A a [ (!1 = 0) -> <!3> comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ -!3) [ (!3 = 1) -> <!4> h a (comp A (p @ !2) [ (!2 = 1) -> <!3> p @ -!3 ]) (\(x : (IdP (<!1> A) a (comp A (p @ !2) [ (!2 = 1) -> <!3> p @ -!3 ])) -> N0) -> efq (IdP (<!3> N0) (x (<!4> comp A a [ (!4 = 1) -> <!3> comp A (p @ (!2 /\ !3)) [ (!2 = 1)(!3 = 1) -> <!4> p @ -!4 ] ])) (x (<!4> comp A a [ (!4 = 1) -> <!3> comp A (p @ (!2 \/ -!3)) [ (!2 = 1) -> <!4> p @ -!4, (!3 = 0) -> <!4> p @ -!4 ] ]))) (x (<!4> comp A a [ (!4 = 1) -> <!5> comp A (p @ (!2 /\ !5)) [ (!2 = 1)(!5 = 1) -> <!6> p @ -!6 ] ])) @ !2) @ !4 ], (!1 = 1) -> <!3> comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ -!3) [ (!3 = 1) -> <!4> h a (comp A (q @ !2) [ (!2 = 1) -> <!3> p @ -!3 ]) (\(x : (IdP (<!1> A) a (comp A (q @ !2) [ (!2 = 1) -> <!3> p @ -!3 ])) -> N0) -> efq (IdP (<!3> N0) (x (<!4> comp A a [ (!4 = 1) -> <!3> comp A (q @ (!2 /\ !3)) [ (!2 = 1)(!3 = 1) -> <!4> p @ -!4 ] ])) (x (<!4> comp A a [ (!4 = 1) -> <!3> comp A (q @ (!2 \/ -!3)) [ (!2 = 1) -> <!4> p @ -!4, (!3 = 0) -> <!4> p @ -!4 ] ]))) (x (<!4> comp A a [ (!4 = 1) -> <!5> comp A (q @ (!2 /\ !5)) [ (!2 = 1)(!5 = 1) -> <!6> p @ -!6 ] ])) @ !2) @ !4 ], (!2 = 0) -> <!3> comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ -!3) [ (!3 = 1) -> <!4> h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !4 ], (!2 = 1) -> <!3> comp A (h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ -!3) [ (!3 = 1) -> <!4> h a a (\(h0 : (IdP (<!0> A) a a) -> N0) -> h0 (<!0> a)) @ !4 ] ]) [ (!2 = 1) -> <!3> p @ !3 ]) [ (!1 = 0) -> <!3> comp A (comp A (p @ !2) [ (!2 = 1) -> <!4> p @ (!3 \/ -!4) ]) [ (!2 = 1) -> <!4> p @ (!3 \/ !4) ], (!1 = 1) -> <!3> comp A (comp A (q @ !2) [ (!2 = 1) -> <!4> p @ (!3 \/ -!4) ]) [ (!2 = 1) -> <!4> p @ (!3 \/ !4) ] ]
+-}
\ No newline at end of file
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index c584fe6..1bfd968 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -146,8 +146,14 @@ data Unit = tt
 data or (A B : U) = inl (a : A)
                   | inr (b : B)
 
+stable (A:U) : U = neg (neg A) -> A
+
 dec (A : U) : U = or A (neg A)
 
+decStable (A:U) : dec A -> stable A = split
+ inl a -> \ (h :neg (neg A)) -> a
+ inr b -> \ (h :neg (neg A)) -> efq A (h b)
+
 discrete (A : U) : U = (a b : A) -> dec (Id A a b)
 
 injective (A B : U) (f : A -> B) : U =