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: https://drops.dagstuhl.de/opus/volltexte/2015/5425/
Capriotti, Paolo ; Kraus, Nicolai ; Vezzosi, Andrea
Functions out of Higher Truncations
| pdf-format: |
|
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 | |
| Seminar: | 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) | |
| Issue date: | 2015 | |
| Date of publication: | 07.09.2015 |
