From 004a01629ab26ff78daa621a6c257da84f92d82c Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 17 Dec 2014 16:36:41 -0500
Subject: [PATCH] feat(hott) add preliminary axiomatized truncation operator

---
 hott/truncation.hlean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 hott/truncation.hlean

diff --git a/hott/truncation.hlean b/hott/truncation.hlean
new file mode 100644
index 000000000..3491a9408
--- /dev/null
+++ b/hott/truncation.hlean
@@ -0,0 +1,19 @@
+-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Jakob von Raumer
+
+open truncation
+
+-- Axiomatize the truncation operator as long as we do not have
+-- Higher inductive types
+
+axiom truncate (A : Type) (n : trunc_index) : Type
+
+axiom truncate.mk {A : Type} (n : trunc_index) (a : A) : truncate A n
+
+axiom truncate.is_trunc (A : Type) (n : trunc_index) : is_trunc n (truncate A n)
+
+axiom truncate.rec_on {A : Type} {n : trunc_index} {C : truncate A n → Type}
+  (ta : truncate A n)
+  [H : Π (ta : truncate A n), is_trunc n (C ta)]
+  (CC : Π (a : A), C (truncate.mk n a)) : C ta