The General Universal Property of the Propositional Truncation
Nicolai Kraus

TL;DR
This paper establishes a universal property for propositional truncation within a type-theoretic framework, generalizing previous results and enabling new ways to define functions from truncated types.
Contribution
It proves a universal property of propositional truncation in a broad type-theoretic setting, extending previous work and simplifying function definitions from truncated types.
Findings
The type of constant functions is equivalent to ||A|| -> B under certain conditions.
The construction can be performed in Homotopy Type Theory.
Finite coherence towers are possible when B is an n-type.
Abstract
In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in Homotopy Type Theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
