The General Universal Property of the Propositional Truncation

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 it streamlines the common approach of finding a proposition Q with A -> Q and Q -> B.