Paolo Capriotti
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.
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/ |
Files
22
(589 Kb)
PDF
Publisher Licence URL
https://creativecommons.org/licenses/by/3.0/
You might also like
Type-theoretic approaches to ordinals
(2023)
Journal Article
A rewriting coherence theorem with applications in homotopy type theory
(2022)
Journal Article
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Conference Proceeding
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
(2019)
Presentation / Conference
Univalent higher categories via complete semi-segal types
(2017)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search