Affordable Access

Constructing the Propositional Truncation using Non-recursive HITs

Authors
  • van Doorn, Floris
Type
Preprint
Publication Date
Dec 07, 2015
Submission Date
Dec 07, 2015
Identifiers
arXiv ID: 1512.02274
Source
arXiv
License
Yellow
External links

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.

Report this publication

Statistics

Seen <100 times