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 -