Sciweavers

CPP
2016

Constructing the propositional truncation using non-recursive HITs

8 years 7 months ago
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
Floris van Doorn
Added 01 Apr 2016
Updated 01 Apr 2016
Type Journal
Year 2016
Where CPP
Authors Floris van Doorn
Comments (0)