From 90a9c20cb57955c637c2983271e70430295d3754 Mon Sep 17 00:00:00 2001 From: Auke Booij Date: Wed, 1 Jun 2016 15:41:30 +0100 Subject: [PATCH] implement propositional truncation --- examples/propTrunc.ctt | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 examples/propTrunc.ctt 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 -- 2.34.1