TY - GEN

T1 - The general universal property of the propositional truncation

AU - Kraus, Nicolai

PY - 2015/10/1

Y1 - 2015/10/1

N2 - In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, ∑, ∐, and identity types), we define the type of coherently constant functions A ∥ ∥ B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over !op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type kAk ! 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 (standard syntactical) homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ∥Ak ∥ →B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A → Q and Q → B.

AB - In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, ∑, ∐, and identity types), we define the type of coherently constant functions A ∥ ∥ B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over !op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type kAk ! 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 (standard syntactical) homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ∥Ak ∥ →B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A → Q and Q → B.

KW - Coherence conditions

KW - Propositional truncation

KW - Reedy limits

KW - Universal property

KW - Well-behaved constancy

UR - http://www.scopus.com/inward/record.url?scp=84975722410&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.TYPES.2014.111

DO - 10.4230/LIPIcs.TYPES.2014.111

M3 - Conference contribution

AN - SCOPUS:84975722410

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 111

EP - 145

BT - 20th International Conference on Types for Proofs and Programs (TYPES 2014)

A2 - Herbelin, Hugo

A2 - Letouzey, Pierre

A2 - Sozeau, Matthieu

PB - Schloss Dagstuhl

T2 - 20th International Conference on Types for Proofs and Programs, TYPES 2014

Y2 - 12 May 2014 through 15 May 2014

ER -