Constructing the Propositional Truncation using Non-recursive HITs

TL;DR

This paper constructs propositional truncation in homotopy type theory using only non-recursive HITs, advancing the understanding of HITs and formalizing the results in Lean proof assistant.

Contribution

It provides a novel construction of propositional truncation via colimits of non-recursive HITs, reducing the need for recursive HITs.

Findings

Constructed propositional truncation using non-recursive HITs

Extended the universal property of propositional truncation

Formalized the results in Lean proof assistant

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.