implement propositional truncation

diff --git a/examples/propTrunc.ctt b/examples/propTrunc.ctt
new file mode 100644 (file)
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> [(i=0) -> x, (i=1) -> y]
+
+pTruncIsProp (A : U) : prop (pTrunc A) =
+ \ (x y : pTrunc A) -> <i> 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
+      (<j> truncP{pTrunc A} x y @ j)
+      (pTruncElim A B pP f x)
+      (pTruncElim A B pP f y)
+    @ i