Functions out of higher truncations

DOI10.4230/LIPICS.CSL.2015.359zbMATH Open1373.03011arXiv1507.01150OpenAlexW2963146135MaRDI QIDQ5351968FDOQ5351968

Authors: Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi 

Publication date: 31 August 2017

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.

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

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

zbMATH Keywords

homotopy type theorytruncation eliminationconstancy on loop spaces

Mathematics Subject Classification ID

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

Cited In (5)

• The general universal property of the propositional truncation
• Truncations of functions
• Title not available (Why is that?)
• Constructions with non-recursive higher inductive types
• A rewriting coherence theorem with applications in homotopy type theory

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)