TY - GEN

T1 - Functions out of higher truncations

AU - Capriotti, Paolo

AU - Kraus, Nicolai

AU - Vezzosi, Andrea

PY - 2015/9/1

Y1 - 2015/9/1

N2 - 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.

AB - 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.

KW - Constancy on loop spaces

KW - Homotopy type theory

KW - Truncation elimination

UR - http://www.scopus.com/inward/record.url?scp=84959300531&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2015.359

DO - 10.4230/LIPIcs.CSL.2015.359

M3 - Conference contribution

AN - SCOPUS:84959300531

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 359

EP - 373

BT - 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

A2 - Kreutzer, Stephan

PB - Schloss Dagstuhl

T2 - 24th EACSL Annual Conference on Computer Science Logic, CSL 2015

Y2 - 7 September 2015 through 10 September 2015

ER -