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.CSL.2015.359
URN: urn:nbn:de:0030-drops-54257
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5425/
Go to the corresponding LIPIcs Volume Portal

Capriotti, Paolo ; Kraus, Nicolai ; Vezzosi, Andrea

Functions out of Higher Truncations

pdf-format:
22.pdf (0.6 MB)

Abstract

In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "set-based" representations of 1-types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda.

BibTeX - Entry

@InProceedings{capriotti_et_al:LIPIcs:2015:5425,
  author =	{Paolo Capriotti and Nicolai Kraus and Andrea Vezzosi},
  title =	{{Functions out of Higher Truncations}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{359--373},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Stephan Kreutzer},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5425},
  URN =		{urn:nbn:de:0030-drops-54257},
  doi =		{10.4230/LIPIcs.CSL.2015.359},
  annote =	{Keywords: homotopy type theory, truncation elimination, constancy on loop spaces}
}

Keywords: homotopy type theory, truncation elimination, constancy on loop spaces
Collection: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Issue Date: 2015
Date of publication: 07.09.2015

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