License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.111
URN: urn:nbn:de:0030-drops-54944
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5494/
Go to the corresponding LIPIcs Volume Portal

Kraus, Nicolai

The General Universal Property of the Propositional Truncation

pdf-format:
8.pdf (0.7 MB)

Abstract

In a type-theoretic 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 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 ||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 =	{111--145},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5494},
  URN =		{urn:nbn:de:0030-drops-54944},
  doi =		{10.4230/LIPIcs.TYPES.2014.111},
  annote =	{Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy}
}

Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI