Document Open Access Logo

Functions out of Higher Truncations

Authors Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.359.pdf
  • Filesize: 0.56 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • homotopy type theory
  • truncation elimination
  • constancy on loop spaces

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) 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 that 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.

Cite As Get BibTex

Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 359-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.359

Author Details

Paolo Capriotti
Nicolai Kraus
Andrea Vezzosi

References

  1. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science (MSCS), pages 1-30, Jan 2015. Google Scholar
  2. Thorsten Altenkirch, Nuo Li, and Ondrej Rypacek. Some constructions on ω-groupoids. In Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), 2014. Google Scholar
  3. Thorsten Altenkirch and Ondrej Rypacek. A syntactical approach to weak ω-groupoids. In Computer Science Logic (CSL), pages 16-30, 2012. Google Scholar
  4. Steve Awodey and Andrej Bauer. Propositions as [types]. Journal of Logic and Computation, 14(4):447-471, 2004. Google Scholar
  5. Paolo Capriotti. Higher lenses. http://homotopytypetheory.org/2014/04/29/higher-lenses/, 29 Apr 2014.
  6. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of higher truncations (Agda formalisation), Apr 2015. Available at URL: https://github.com/pcapriotti/agda-base/tree/trunc/hott/truncation.
  7. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, NJ, 1986. Google Scholar
  8. Nicolai Kraus. The general universal property of the propositional truncation. ArXiv e-prints, Nov 2014. To appear in the post-proceedings of TYPES'14. Google Scholar
  9. Nicolai Kraus. Truncation Levels in Homotopy Type Theory. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2015. Google Scholar
  10. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Löf type theory. Submitted, 2014. Google Scholar
  11. Nicolai Kraus and Christian Sattler. Higher homotopies in a hierarchy of univalent universes. ACM Transactions on Computational Logic (TOCL), 16(2):18:1-18:12, April 2015. Google Scholar
  12. Peter LeFanu Lumsdaine. Weak omega-categories from intensional type theory. In Typed Lambda Calculi and Applications (TLCA), pages 172-187. Springer-Verlag, 2009. Google Scholar
  13. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, pages 1-75, Jan 2015. Google Scholar
  14. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study, first edition, 2013.
  15. Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact