Constructing the Propositional Truncation using Non-recursive HITs
Logic
2015-12-09 v1
Abstract
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.
Cite
@article{arxiv.1512.02274,
title = {Constructing the Propositional Truncation using Non-recursive HITs},
author = {Floris van Doorn},
journal= {arXiv preprint arXiv:1512.02274},
year = {2015}
}
Comments
8 pages, Certified Programs and Proofs 2016