Functions out of higher truncations

Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

In homotopy type theory, the truncation operator ||-||n (for a number n ≥ -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 which 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.

Original languageEnglish
Title of host publication24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
EditorsStephan Kreutzer
PublisherSchloss Dagstuhl
Pages359-373
ISBN (Electronic)9783939897903
DOIs
Publication statusPublished - 1 Sep 2015
Event24th EACSL Annual Conference on Computer Science Logic, CSL 2015 - Berlin, Germany
Duration: 7 Sep 201510 Sep 2015

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume41
ISSN (Print)1868-8969

Conference

Conference24th EACSL Annual Conference on Computer Science Logic, CSL 2015
Country/TerritoryGermany
CityBerlin
Period7/09/1510/09/15

Keywords

  • Constancy on loop spaces
  • Homotopy type theory
  • Truncation elimination

ASJC Scopus subject areas

  • Software

Cite this