Functions out of Higher Truncations

Capriotti, Paolo; Kraus, Nicolai; Vezzosi, Andrea

Abstract

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

Citation

Capriotti, P., Kraus, N., & Vezzosi, A. (2015). Functions out of Higher Truncations. LIPIcs, 41, https://doi.org/10.4230/LIPIcs.CSL.2015.359

• Journal Article Type: Article
• Conference Name: 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
• Online Publication Date: Sep 7, 2015
• Publication Date: Sep 7, 2015
• Deposit Date: Jul 15, 2020
• Publicly Available Date: Jul 27, 2020
• Journal: Leibniz International Proceedings in Informatics (LIPIcs)
• Peer Reviewed: Peer Reviewed
• Volume: 41
• DOI: https://doi.org/10.4230/LIPIcs.CSL.2015.359
• Keywords: Logic in Computer Science; Logic
• Public URL: https://nottingham-repository.worktribe.com/output/2461922
• Publisher URL: https://drops.dagstuhl.de/opus/volltexte/2015/5425/