From cde2f940f123bedcb5b461691b08a676e2a04875 Mon Sep 17 00:00:00 2001 From: coquand Date: Tue, 21 Apr 2015 16:57:12 +0200 Subject: [PATCH] updated proofs of Hedberg's Theorem --- examples/newhedberg.ctt | 22 +++++++++++---- examples/other.ctt | 62 +++++++++++++++++++++++++++++++++++++++++ examples/prelude.ctt | 6 ++++ 3 files changed, 84 insertions(+), 6 deletions(-) create mode 100644 examples/other.ctt 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) -> 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 (Square A a a (refl A a) a (p@i) (p@i/\j) (f a (refl A a)) (f (p@i) (p@i/\j))) ((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 = 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 ( A) a x) -> N0) -> N0) -> (IdP ( A) a x)) -> + \(a b : A) -> + \(p q : IdP ( A) a b) -> + comp A a [ (!0 = 0) -> comp A (comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !2) [ (!2 = 1) -> p @ (!3 /\ !1) ]) [ (!1 = 1) -> comp A (h a (p @ !3) (\(h0 : (IdP ( A) a (p @ !3)) -> N0) -> h0 ( p @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> p @ (!3 \/ !4) ] ], (!0 = 1) -> comp A (comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !2) [ (!2 = 1) -> q @ (!3 /\ !1) ]) [ (!1 = 1) -> comp A (h a (q @ !3) (\(h0 : (IdP ( A) a (q @ !3)) -> N0) -> h0 ( q @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> q @ (!3 \/ !4) ] ], (!1 = 0) -> h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !2, (!1 = 1) -> h a b (\(x : (IdP ( A) a b) -> N0) -> efq (IdP ( 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 ((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 = (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 = (p@i,(lemPropF A P pP a a p na na)@i) + g (p:B) : Id A a a = (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 (prop (Id A a (p@i))) (h a) p q + +{- + \(A : U) -> + \(h : (a : A) -> (a0 : IdP ( A) a a) -> (b : IdP ( A) a a) -> IdP ( IdP ( A) a a) a0 b) -> + \(a : A) -> + \(b : A) -> + \(p : IdP ( A) a b) -> \(q : IdP ( A) a b) -> + comp A (comp A (h a ( comp A (p @ j) [ (j = 1) -> p @ -i ]) ( comp A (q @ j) [ (j = 1) -> p @ -i ]) @ j @ k) [ (k = 1) -> p @ i ]) [ (j = 0) -> comp A (comp A (p @ k) [ (k = 1) -> p @ (i \/ -j) ]) [ (k = 1) -> p @ (i \/ j) ], (j = 1) -> comp A (comp A (q @ k) [ (k = 1) -> p @ (i \/ -j) ]) [ (k = 1) -> 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 ( A) a x) -> N0) -> N0) -> (IdP ( A) a x)) -> + \(a b : A) -> + \(p q : IdP ( A) a b) -> + comp A (comp A (comp A a [ (!1 = 0) -> comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ -!3) [ (!3 = 1) -> h a (comp A (p @ !2) [ (!2 = 1) -> p @ -!3 ]) (\(x : (IdP ( A) a (comp A (p @ !2) [ (!2 = 1) -> p @ -!3 ])) -> N0) -> efq (IdP ( N0) (x ( comp A a [ (!4 = 1) -> comp A (p @ (!2 /\ !3)) [ (!2 = 1)(!3 = 1) -> p @ -!4 ] ])) (x ( comp A a [ (!4 = 1) -> comp A (p @ (!2 \/ -!3)) [ (!2 = 1) -> p @ -!4, (!3 = 0) -> p @ -!4 ] ]))) (x ( comp A a [ (!4 = 1) -> comp A (p @ (!2 /\ !5)) [ (!2 = 1)(!5 = 1) -> p @ -!6 ] ])) @ !2) @ !4 ], (!1 = 1) -> comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ -!3) [ (!3 = 1) -> h a (comp A (q @ !2) [ (!2 = 1) -> p @ -!3 ]) (\(x : (IdP ( A) a (comp A (q @ !2) [ (!2 = 1) -> p @ -!3 ])) -> N0) -> efq (IdP ( N0) (x ( comp A a [ (!4 = 1) -> comp A (q @ (!2 /\ !3)) [ (!2 = 1)(!3 = 1) -> p @ -!4 ] ])) (x ( comp A a [ (!4 = 1) -> comp A (q @ (!2 \/ -!3)) [ (!2 = 1) -> p @ -!4, (!3 = 0) -> p @ -!4 ] ]))) (x ( comp A a [ (!4 = 1) -> comp A (q @ (!2 /\ !5)) [ (!2 = 1)(!5 = 1) -> p @ -!6 ] ])) @ !2) @ !4 ], (!2 = 0) -> comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ -!3) [ (!3 = 1) -> h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !4 ], (!2 = 1) -> comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ -!3) [ (!3 = 1) -> h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !4 ] ]) [ (!2 = 1) -> p @ !3 ]) [ (!1 = 0) -> comp A (comp A (p @ !2) [ (!2 = 1) -> p @ (!3 \/ -!4) ]) [ (!2 = 1) -> p @ (!3 \/ !4) ], (!1 = 1) -> comp A (comp A (q @ !2) [ (!2 = 1) -> p @ (!3 \/ -!4) ]) [ (!2 = 1) -> 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 = -- 2.34.1