Functions out of higher truncations

DOI10.4230/LIPICS.CSL.2015.359MaRDI QIDQ5351968zbMATH OpenOpenAlexFDO

Authors Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi

Publication date 31 August 2017

Full work available at URL https://arxiv.org/abs/1507.01150

zbMATH Keywords

homotopy type theorytruncation eliminationconstancy on loop spaces

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

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.

Recommendations

• The general universal property of the propositional truncation
• Constructions with non-recursive higher inductive types
• Higher homotopies in a hierarchy of univalent universes
• Partial univalence in \(n\)-truncated type theory
• Semantics of higher inductive types

Cited in

(5)

• The general universal property of the propositional truncation
• scientific article; zbMATH DE number 3935736 (Why is no real title available?)
• A rewriting coherence theorem with applications in homotopy type theory
• Truncations of functions
• Constructions with non-recursive higher inductive types

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Functions out of higher truncations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5351968)