From: Auke Booij Date: Wed, 1 Jun 2016 14:41:30 +0000 (+0100) Subject: implement propositional truncation X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=90a9c20cb57955c637c2983271e70430295d3754;p=cubicaltt.git implement propositional truncation --- diff --git a/examples/propTrunc.ctt b/examples/propTrunc.ctt new file mode 100644 index 0000000..8ea8f7f --- /dev/null +++ b/examples/propTrunc.ctt @@ -0,0 +1,26 @@ +module propTrunc where + +import prelude + +data pTrunc (A : U) + = inc (a : A) + | truncP (x y : pTrunc A) [(i=0) -> x, (i=1) -> y] + +pTruncIsProp (A : U) : prop (pTrunc A) = + \ (x y : pTrunc A) -> truncP{pTrunc A} x y @ i + +pTruncRec (A B : U) (pP : prop B) (f : A -> B) : pTrunc A -> B = split + inc a -> f a + truncP x y @ i -> pP (pTruncRec A B pP f x) (pTruncRec A B pP f y) @ i + +pTruncElim (A : U) (B : (pTrunc A) -> U) + (pP : (x : pTrunc A) -> prop (B x)) + (f : (a : A) -> B (inc a)) + : (x : pTrunc A) -> B x = split + inc a -> f a + truncP x y @ i -> + lemPropF (pTrunc A) B pP x y + ( truncP{pTrunc A} x y @ j) + (pTruncElim A B pP f x) + (pTruncElim A B pP f y) + @ i