Sökning: onr:"swepub:oai:research.chalmers.se:9bd5ada0-b660-4ea0-9fb7-aa007b024cfe" >
Functions out of Hi...
Functions out of Higher Truncations
-
- Capriotti, Paolo (författare)
- University Of Nottingham
-
- Kraus, Nicolai (författare)
- University Of Nottingham
-
- Vezzosi, Andrea, 1986 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- ISBN 9783939897903
- 2015
- 2015
- Engelska.
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783939897903 ; 41, s. 359-373
- Relaterad länk:
-
http://dx.doi.org/10...
-
visa fler...
-
https://research.cha...
-
https://doi.org/10.4...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- constancy on loop spaces
- homotopy type theory
- truncation elimination
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas