From: coquand Date: Wed, 29 Apr 2015 07:50:57 +0000 (+0200) Subject: more efficient version of groupoid truncation X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=48b40fcc053d14fd63d204083eef6b062a14b609;p=cubicaltt.git more efficient version of groupoid truncation --- diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt index 4ce230b..a166486 100644 --- a/examples/groupoidTrunc.ctt +++ b/examples/groupoidTrunc.ctt @@ -42,7 +42,7 @@ lem (A:U) (P:A -> U) (gP:(x:A) -> groupoid (P x)) (a :A) : (b:A) (p q:Id A a b) (r s:Id (Id A a b) p q) (t:Id (Id (Id A a b) p q) r s) (a1:P a) (b1:P b) (p1: IdP (P (p@i)) a1 b1) (q1: IdP (P (q@i)) a1 b1) (r1 : IdP (IdP (P (r@i@j)) a1 b1) p1 q1) (s1 : IdP (IdP (P (s@i@j)) a1 b1) p1 q1) -> - IdP (IdP (IdP (P (t@i@j@k)) a1 b1) p1 q1) r1 s1 = + IdP (IdP (IdP (P (t@i@j@k)) a1 b1) p1 q1) r1 s1 = J A a (\ (b:A) (p :Id A a b) -> (q:Id A a b) (r s:Id (Id A a b) p q) (t:Id (Id (Id A a b) p q) r s) (a1:P a) (b1:P b) (p1: IdP (P (p@i)) a1 b1) (q1: IdP (P (q@i)) a1 b1) (r1 : IdP (IdP (P (r@i@j)) a1 b1) p1 q1) (s1 : IdP (IdP (P (s@i@j)) a1 b1) p1 q1) -> @@ -58,19 +58,35 @@ lem (A:U) (P:A -> U) (gP:(x:A) -> groupoid (P x)) (r1 : IdP (IdP (P (r@i@j)) a1 b1) p1 q1) (s1 : IdP (IdP (P (s@i@j)) a1 b1) p1 q1) -> IdP (IdP (IdP (P (t@i@j@k)) a1 b1) p1 q1) r1 s1) (lem1 A P gP a) -gTruncElim (A : U) +T:U = (A:U) (P:A -> U) (gP:(x:A) -> groupoid (P x)) + (a b:A) (p q:Id A a b) (r s:Id (Id A a b) p q) (t:Id (Id (Id A a b) p q) r s) + (a1:P a) (b1:P b) (p1: IdP (P (p@i)) a1 b1) (q1: IdP (P (q@i)) a1 b1) + (r1 : IdP (IdP (P (r@i@j)) a1 b1) p1 q1) (s1 : IdP (IdP (P (s@i@j)) a1 b1) p1 q1) -> + IdP (IdP (IdP (P (t@i@j@k)) a1 b1) p1 q1) r1 s1 + +gTruncElim1 (lem:T) (A : U) (B : (gTrunc A) -> U) (bG : (z:gTrunc A) -> groupoid (B z)) (f : (x:A) -> B (inc x)) : (z:gTrunc A) -> B z = split inc a -> f a squashC a b p q r s @ i j k -> lem (gTrunc A) B bG a b p q r s (gTr A a b p q r s) - (gTruncElim A B bG f a) - (gTruncElim A B bG f b) - ( gTruncElim A B bG f (p @ m)) - ( gTruncElim A B bG f (q @ m)) - ( gTruncElim A B bG f (r @ m @ n)) - ( gTruncElim A B bG f (s @ m @ n)) @ i @ j @ k + (gTruncElim1 lem A B bG f a) + (gTruncElim1 lem A B bG f b) + ( gTruncElim1 lem A B bG f (p @ m)) + ( gTruncElim1 lem A B bG f (q @ m)) + ( gTruncElim1 lem A B bG f (r @ m @ n)) + ( gTruncElim1 lem A B bG f (s @ m @ n)) @ i @ j @ k + +gTruncElim : (A : U) + (B : (gTrunc A) -> U) + (bG : (z:gTrunc A) -> groupoid (B z)) + (f : (x:A) -> B (inc x)) (z:gTrunc A) -> B z = gTruncElim1 lem + + + + + setGroupoid (A:U) (h:set A) (a b:A) : set (Id A a b) = propSet (Id A a b) (h a b)