The General Universal Property of the Propositional Truncation
arXiv:1411.2682 · doi:10.4230/LIPIcs.TYPES.2014.111
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 it streamlines the common approach of finding a proposition Q with A -> Q and Q -> B.
v1: 27 pages; v2: 34 pages, improved notation, improved presentation in general, added figures to improve readability, added proof for the finite cases, corrected conjecture; to appear in the post-proceedings of TYPES'14 (LIPIcs); v3: fixed the statement of Lemma 2.1