### Skapa referens, olika format (klipp och klistra)

**Harvard**

Capriotti, P., Kraus, N. och Vezzosi, A. (2015) *Functions out of Higher Truncations *.

** BibTeX **

@conference{

Capriotti2015,

author={Capriotti, Paolo and Kraus, Nicolai and Vezzosi, Andrea},

title={Functions out of Higher Truncations },

booktitle={24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},

isbn={978-3-939897-90-3},

pages={359-373},

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.
},

year={2015},

keywords={homotopy type theory, truncation elimination, constancy on loop spaces },

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 227466

A1 Capriotti, Paolo

A1 Kraus, Nicolai

A1 Vezzosi, Andrea

T1 Functions out of Higher Truncations

YR 2015

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

SN 978-3-939897-90-3

SP 359

OP 373

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

LA eng

DO 10.4230/LIPIcs.CSL.2015.359

LK http://dx.doi.org/10.4230/LIPIcs.CSL.2015.359

OL 30