From: Anders Date: Thu, 23 Apr 2015 15:04:00 +0000 (+0200) Subject: Elimination principle for set truncation X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d3d379d409da3e43543e1869915e07aea893b323;p=cubicaltt.git Elimination principle for set truncation --- diff --git a/examples/set.ctt b/examples/set.ctt new file mode 100644 index 0000000..04607a6 --- /dev/null +++ b/examples/set.ctt @@ -0,0 +1,54 @@ +module set where + +sqDepPath (A:U) (F:A->U) (sF:(x:A) -> set (F x)) + (a0 a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP ( F (p@i)) u0 u1) : + Id (IdP ( F (p@i)) u0 u1) q r = rem @ j @ i + where + rem : IdP (Id (F (p@i)) (q@i) (r@i)) (u0) (u1) = + let xi : A = p@i + ui0 : F xi = transport (F (p @ i/\j)) u0 + ui1 : F xi = transport (F (p @ i\/-j)) u1 + qi : Id (F xi) ui0 ui1 = transport (F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (q@j) + ri : Id (F xi) ui0 ui1 = transport (F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (r@j) + in (sF xi ui0 ui1 qi ri @ j @ i) + +sqDepPathJ (A:U) (F:A->U) (sF:(x:A) -> set (F x)) + (a0 : A) : (a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP ( F (p@i)) u0 u1) -> + Id (IdP ( F (p@i)) u0 u1) q r = + J A a0 (\ (a1:A) (p:Id A a0 a1) -> (u0 : F a0) (u1 : F a1) (q r: IdP ( F (p@i)) u0 u1) -> + Id (IdP ( F (p@i)) u0 u1) q r) (sF a0) + +test (A:U) (F:A->U) (sF:(x:A) -> set (F x)) + (a0 a1:A) (p:Id A a0 a1) (u0 : F a0) (u1 : F a1) (q r: IdP ( F (p@i)) u0 u1) : + Id (IdP ( F (p@i)) u0 u1) q r = sqDepPathJ A F sF a0 a1 p u0 u1 q r + +sqDepPath2 (A:U) (F:A->U) (sF:(x:A) -> set (F x)) + (a0 a1:A) (p :Id A a0 a1) : (q : Id A a0 a1) (spq : Id (Id A a0 a1) p q) + (u0 : F a0) (u1 : F a1) + (r : IdP ( F (p@i)) u0 u1) (s : IdP ( F (q@i)) u0 u1) -> + IdP ( IdP ( F (spq @ i @ j)) u0 u1) r s = + J (Id A a0 a1) p + (\(q : Id A a0 a1) (spq : Id (Id A a0 a1) p q) -> + (u0 : F a0) (u1 : F a1) (r : IdP ( F (p@i)) u0 u1) + (s : IdP ( F (q@i)) u0 u1) -> IdP ( IdP ( F (spq @ i @ j)) u0 u1) r s) rem + where rem : (u0 : F a0) (u1 : F a1) (r s : IdP ( F (p@i)) u0 u1) -> + Id (IdP ( F (p @ j)) u0 u1) r s = sqDepPath A F sF a0 a1 p + +-- rem @ j @ i +-- where +-- rem : IdP ( IdP ( F (spq @ j @ i)) (r@i) (s@i)) (u0) (u1) = +-- let xi : A = p @ i +-- yi : A = q @ i +-- li : Id A xi yi = spq @ j @ i +-- ui0 : F xi = transport (F (p @ i/\j)) u0 +-- ui1 : F xi = transport (F (p @ i\/-j)) u1 +-- vi0 : F yi = transport (F (q @ i/\j)) u0 +-- vi1 : F yi = transport (F (q @ i\/-j)) u1 +-- ri : Id (F xi) ui0 ui1 = transport (F (p@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (r@j) +-- si : Id (F yi) vi0 vi1 = transport (F (q@(i/\-j/\k)\/(i/\j)\/(j/\-k)\/(i/\k))) (s@j) +-- uvi0 : IdP ( F (li @ j)) ui0 vi0 = transport +-- uvi1 : IdP ( F (li @ j)) ui1 vi1 = +-- test : U = U +-- in (sF xi ui0 ui1 ri si @ j @ i) + + diff --git a/examples/setTrunc.ctt b/examples/setTrunc.ctt index bd34fba..e9abf8b 100644 --- a/examples/setTrunc.ctt +++ b/examples/setTrunc.ctt @@ -1,18 +1,21 @@ module setTrunc where -import prelude +import set data setTrunc (A : U) = inc (a : A) - | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) + | setTrC (a b : setTrunc A) (p q : Id (setTrunc A) a b) [ (i=0) -> p @ j , (i=1) -> q @ j , (j=0) -> a , (j=1) -> b] -setTruncSet (A : U) : set (setTrunc A) = - \(a b : setTrunc A) (p q : Id (setTrunc A) a b) -> - setTr {setTrunc A} a b p q @ i @ j +setTr (A : U) (a b : setTrunc A) (p q : Id (setTrunc A) a b) : Id (Id (setTrunc A) a b) p q = + setTrC {setTrunc A} a b p q @ i @ j + +-- setTruncSet (A : U) : set (setTrunc A) = +-- \(a b : setTrunc A) (p q : Id (setTrunc A) a b) -> +-- setTrC {setTrunc A} a b p q @ i @ j setTruncRec (A : U) @@ -22,7 +25,14 @@ setTruncRec (A : U) setTrunc A -> B = split inc a -> f a - setTr a b p q @ i j -> (bS (setTruncRec A B bS f a) + setTrC a b p q @ i j -> (bS (setTruncRec A B bS f a) (setTruncRec A B bS f b) ( setTruncRec A B bS f (p @ k)) ( setTruncRec A B bS f (q @ k))) @ i @ j + +setTruncElim (A : U) (P : setTrunc A -> U) (sP : (z : setTrunc A) -> set (P z)) (h : (x : A) -> P (inc x)) + : (z : setTrunc A) -> P z = split + inc a -> h a + setTrC a b p q @ i j -> sqDepPath2 (setTrunc A) P sP a b p q (setTr A a b p q) + (f a) (f b) ( f (p @ k)) ( f (q @ k)) @ i @ j + where f : (z : setTrunc A) -> P z = setTruncElim A P sP h \ No newline at end of file