CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Functions out of Higher Truncations

Paolo Capriotti ; Nicolai Kraus ; Andrea Vezzosi (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (1868-8969). Vol. 41 (2015), p. 359-373.
[Konferensbidrag, refereegranskat]

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.

Nyckelord: homotopy type theory, truncation elimination, constancy on loop spaces

Denna post skapades 2015-12-07. Senast ändrad 2016-03-23.
CPL Pubid: 227466


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)


Teoretisk datalogi

Chalmers infrastruktur