Constructing the Propositional Truncation using Non-recursive HITs
From MaRDI portal
(Redirected from Publication:6268151)
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 page was built for publication: Constructing the Propositional Truncation using Non-recursive HITs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6268151)
