In the homotopical reading of Martin-Löf type theory, the propositional truncation of a type is a type that has two key properties:
Recall that a mere proposition is a type for which we have an inhabitant
Recall also that we have always a function
from to its propositional truncation.
The propositional truncation of a type has the following universal property: for every mere proposition , and any function , there exists a unique function (the dotted line) that makes the following diagram commute:
Please add universal property in terms of type-theoretic equivalences.
The propositional truncation of a type can be defined as a higher inductive type (HIT).
This is originally due to [Lumsdaine and Shulman 2014] (still unpublished?).
A textbook account can be found in the HoTT book.
The propositional truncation of a type can also be defined through an impredicative encoding. Assuming we have a universe of propositions, this is given by
Two things to remember about this: