Capriotti, Paolo ;
Kraus, Nicolai ;
Vezzosi, Andrea
Functions out of Higher Truncations
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 ntypes, which makes it hard to construct functions An > B if B is not an ntype. 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 An > 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 "setbased" representations of 1types, 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 = {359373},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897903},
ISSN = {18688969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5425},
URN = {urn:nbn:de:0030drops54257},
doi = {10.4230/LIPIcs.CSL.2015.359},
annote = {Keywords: homotopy type theory, truncation elimination, constancy on loop spaces}
}
2015
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: 

2015 