Constructing the propositional truncation using non-recursive HITs

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean. Categories and Subject Descriptors F.4.1 [Mathematical Logic] Keywords Homotopy Type Theory, Propositional Truncation, Higher Inductive Types, Lean

• Type: Journal
• Year: 2016
• Where: CPP
• Authors: Floris van Doorn
• Keywords: Artificial Intelligence, CPP 2016