Papers With

← All papers
First page of Constructing the Propositional Truncation using Non-recursive HITs

Constructing the Propositional Truncation using Non-recursive HITs

Floris van Doorn

math.LO Dec 7, 2015 · v1
formalization type-theory topology logic
Read PDF arXiv abstract
TL;DR
Formalizes a colimit construction of propositional truncation from non-recursive HITs in Lean.
Abstract
In homotopy type theory, the propositional truncation is constructed as a colimit using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. The construction also characterizes functions from the propositional truncation to arbitrary types, extending its universal property. The results are formalized in the Lean proof assistant.
Problem

In homotopy type theory, the propositional truncation is typically defined as a recursive higher inductive type (HIT). Whether it can be constructed from non-recursive HITs alone was an open question, relevant to reducing the foundational assumptions of HoTT.

Approach

The authors construct the propositional truncation as a colimit using only non-recursive higher inductive types. The construction characterizes functions from the propositional truncation to arbitrary types, extending its universal property. The results are formalized in the Lean proof assistant.

Results

The propositional truncation is successfully constructed without recursive HITs, providing a first step toward reducing recursive HITs to non-recursive ones. The extended universal property characterizes all functions out of the truncation, not just those into propositions.