Functions out of Higher Truncations

TL;DR

This paper develops new elimination principles for higher truncations in homotopy type theory, enabling more flexible function constructions and applications to set-based representations of 1-types with braided loop spaces.

Contribution

It introduces a general theorem linking functions out of higher truncations to constant functions on loop spaces, with formal proofs in Agda.

Findings

Functions from ||A||n to (n+1)-types correspond to constant functions on (n+1)-loop spaces.

Allows construction of set-based representations of 1-types with braided loop spaces.

Formalized proofs in Agda demonstrate the results.

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.