pith. sign in

arxiv: 1512.02274 · v1 · pith:HSAVMKUNnew · submitted 2015-12-07 · 🧮 math.LO

Constructing the Propositional Truncation using Non-recursive HITs

Floris van Doorn This is my paper
classification 🧮 math.LO
keywords hitspropositionaltruncationnon-recursivetypearbitraryassistantcharacterization
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Classifying Types

    math.LO 2019-06 unverdicted novelty 5.0

    The thesis advances the development of synthetic homotopy theory within homotopy type theory, covering classifying types and internal questions not necessarily tied to classical homotopy.