Document Open Access Logo

Extending Homotopy Type Theory with Strict Equality

Authors Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.21.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Author Details

Thorsten Altenkirch
Paolo Capriotti
Nicolai Kraus

Cite AsGet BibTex

Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.21

Abstract

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an "outer" one, containing a strict equality type former, and an "inner" one, which is some version of HoTT. Our type theory is inspired by Voevodsky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we do not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of "infinite structures" which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with "schematic" definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
Keywords
  • homotopy type theory
  • coherences
  • strict equality
  • homotopy type system

Metrics

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

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. URL: http://dx.doi.org/10.1017/S0960129514000486.
  2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg. Towards a theory of higher inductive types. Presentation at TYPES'15, Tallinn, Estonia, 20 May 2015. Google Scholar
  3. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Infinite structures in type theory: Problems and approaches. Presented at TYPES'15, Tallinn, Estonia, 20 May 2015. Google Scholar
  4. Andrej Bauer, Gaëtan Gilbert, Philipp Haselwarter, Matija Pretnar, and Chris Stone. Andromeda. Implementation of a type theory with equality reflection, ongoing project. URL: http://andromedans.github.io/andromeda/.
  5. Paolo Capriotti. Models of Type Theory with Strict Equality. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2016. In preparation. Google Scholar
  6. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs (TYPES), volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer-Verlag, 1995. URL: http://dx.doi.org/10.1007/3-540-61780-9_66.
  7. Yonatan Harpaz. Quasi-unital ∞-categories. Algebraic &Geometric Topology, 15(4):2303-2381, 2015. Google Scholar
  8. Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science (MSCS), pages 1-16, Mar 2015. URL: http://dx.doi.org/10.1017/S0960129514000528.
  9. Martin Hofmann. Conservativity of equality reflection over intensional type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs (TYPES), volume 1158 of Lecture Notes in Computer Science, pages 153-164. Springer-Verlag, 1995. URL: http://dx.doi.org/10.1007/3-540-61780-9_68.
  10. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  11. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Venice Festschrift, pages 83-111. Oxford University Press, 1996. Google Scholar
  12. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations. ArXiv e-prints, Nov 2012. Google Scholar
  13. Nicolai Kraus. The general universal property of the propositional truncation. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, Types for Proofs and Programs (TYPES), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 111-145, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2014.111.
  14. Nicolai Kraus. Truncation Levels in Homotopy Type Theory. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2015. Google Scholar
  15. Peter LeFanu Lumsdaine. Higher Categories from Type Theories. PhD thesis, Carnegie Mellon University, 2010. Google Scholar
  16. Jacob Lurie. Higher Topos Theory. Annals of Mathematics Studies. Princeton University Press, Princeton, 2009. Google Scholar
  17. Maria Emilia Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009. Computation and Logic in the Real World: CiE 2007. URL: http://dx.doi.org/10.1016/j.apal.2009.01.006.
  18. Fedor Part and Zhaohui Luo. Semi-simplicial types in logic-enriched homotopy type theory. CoRR, abs/1506.04998, 2015. URL: http://arxiv.org/abs/1506.04998.
  19. Michael Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow). http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/, 3 Mar 2014.
  20. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, pages 1-75, Jan 2015. URL: http://dx.doi.org/10.1017/S0960129514000565.
  21. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book/.
  22. Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. URL: http://dx.doi.org/10.1112/plms/pdq026.
  23. Vladimir Voevodsky. A simple type system with two identity types, 2013. Unpublished note. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact