Kraus, Nicolai
The General Universal Property of the Propositional Truncation
Abstract
In a typetheoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently 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^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 A > B. If B is an ntype 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 A > 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.
BibTeX  Entry
@InProceedings{kraus:LIPIcs:2015:5494,
author = {Nicolai Kraus},
title = {{The General Universal Property of the Propositional Truncation}},
booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)},
pages = {111145},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897880},
ISSN = {18688969},
year = {2015},
volume = {39},
editor = {Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5494},
URN = {urn:nbn:de:0030drops54944},
doi = {10.4230/LIPIcs.TYPES.2014.111},
annote = {Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, wellbehaved constancy}
}
2015
Keywords: 

coherence conditions, propositional truncation, Reedy limits, universal property, wellbehaved constancy 
Seminar: 

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

Issue date: 

2015 
Date of publication: 

2015 