Document Open Access Logo

Internal Universes in Models of Homotopy Type Theory

Authors Daniel R. Licata , Ian Orton , Andrew M. Pitts , Bas Spitters

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.22.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Author Details

Daniel R. Licata
  • Wesleyan University Dept. Mathematics & Computer Science, Middletown, USA
Ian Orton
  • University of Cambridge Dept. Computer Science & Technology, Cambridge, UK
Andrew M. Pitts
  • University of Cambridge Dept. Computer Science & Technology, Cambridge, UK
Bas Spitters
  • Aarhus University Dept. Computer Science, Aarhus, DK

Funding

  • Licata, Daniel R.: Supported by United States Air Force Research Laboratory, agreement numbers FA-95501210370 and FA-95501510053.
  • Orton, Ian: Supported by a UK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.
  • Spitters, Bas: Supported by the Guarded Homotopy Type Theory project, funded by the Villum Foundation, project number 12386.

Cite As Get BibTex

Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSCD.2018.22

Abstract

We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these model are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mörtberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • cubical sets
  • dependent type theory
  • homotopy type theory
  • internal language
  • modalities
  • univalent foundations
  • universes

Metrics

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

Related Versions

Supplementary Materials

References

  1. P. Aczel. On relating type theories and set theories. In Proc. TYPES 1998, volume 1657 of Lecture Notes in Computer Science, pages 1-18, 1999. Google Scholar
  2. Agda-flat. URL: https://github.com/agda/agda/tree/flat.
  3. Agda Project. URL: https://wiki.portal.chalmers.se/agda.
  4. T. Altenkirch, P. Capriotti, and N. Kraus. Extending homotopy type theory with strict equality, 2016. URL: http://arxiv.org/abs/1604.03799.
  5. C. Angiuli, G. Brunerie, T. Coquand, K.-B. Hou (Favonia), R. Harper, and D. R. Licata. Cartesian cubical type theory, 2017. URL: https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf.
  6. C. Angiuli, K.-B. Hou (Favonia), and R. Harper. Computational higher type theory III: univalent universes and exact equality, 2017. URL: http://arxiv.org/abs/1712.01800.
  7. S. Awodey. Notes on cubical models of type theory, 2016. URL: https://github.com/awodey/math/blob/master/Cubical/cubical.pdf.
  8. R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, 1975. Google Scholar
  9. M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107-128, 2014. Google Scholar
  10. L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory. Journal of Automated Reasoning, 2018. Google Scholar
  11. U. Buchholtz and E. Morehouse. Varieties of cubical sets. In Relational and Algebraic Methods in Computer Science: 16th International Conference (RAMiCS 2017), Proceedings, 2017. Google Scholar
  12. R. Clouston, B. Mannaa, R. E. Møgelberg, A. M. Pitts, and B. Spitters. Modal dependent type theory and dependent right adjoints. arXiv:1804.05236, 2018. Google Scholar
  13. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In T. Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  14. V. de Paiva and E. Ritter. Fibrational modal type theory. Electronic Notes in Theoretical Computer Science, 323:143-161, 2016. Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015). Google Scholar
  15. P. Dybjer. Internal type theory. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer Berlin Heidelberg, 1996. Google Scholar
  16. D. Frumin and B. Van Den Berg. A homotopy-theoretic model of function extensionality in the effective topos. Mathematical Structures in Computer Science, 2018. To appear. Google Scholar
  17. N. Gambino and C. Sattler. The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, 221:3027-3068, 2017. Google Scholar
  18. M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995. Google Scholar
  19. M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, Publications of the Newton Institute, pages 79-130. Cambridge University Press, 1997. Google Scholar
  20. M. Hofmann and T. Streicher. Lifting Grothendieck universes. Unpublished note, 1999. Google Scholar
  21. P. T. Johnstone. Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2. Number 43-44 in Oxford Logic Guides. Oxford University Press, 2002. Google Scholar
  22. C. Kapulkin and P. L. Lumsdaine. The simplicial model of univalent foundations (after Voedodsky). arXiv:1211.2851v4, jun 2016. Google Scholar
  23. F. W. Lawvere. Toward the description in a smooth topos of the dynamically possible motions and deformations of a continuous body. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 21(4):377-392, 1980. Google Scholar
  24. F. W. Lawvere. Axiomatic cohesion. Theory and Applications of Categories, 19(3):41-49, 2007. Google Scholar
  25. Z. Luo. Notes on universes in type theory. Lecture notes for a talk at the Institute for Advanced Study, Princeton, 2012. Google Scholar
  26. S. MacLane. Categories for the Working Mathematician. Graduate Texts in Mathematics 5. Springer, 1971. Google Scholar
  27. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984. Google Scholar
  28. A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. ACM Trans. Comput. Logic, 9(3):23:1-23:49, 2008. Google Scholar
  29. A. Nuyts, A. Vezzosi, and D. Devriese. Parametric quantifiers for dependent type theory. Proc. ACM Program. Lang., 1(ICFP):32:1-32:29, aug 2017. Google Scholar
  30. I. Orton and A. M. Pitts. Axioms for modelling cubical type theory in a topos. In Proc. CSL 2016, volume 62 of LIPIcs, pages 24:1-24:19, 2016. Google Scholar
  31. I. Orton and A. M. Pitts. Decomposing the univalence axiom. arXiv:1712.04890, dec 2017. Google Scholar
  32. I. Orton and A. M. Pitts. Axioms for modelling cubical type theory in a topos. Logical Methods in Computer Science, 2018. Special issue for CSL 2016, to appear; arXiv:1712.04864. Revised and expanded version of [30]. Google Scholar
  33. F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001. Google Scholar
  34. E. Riehl and M. Shulman. A type theory for synthetic ∞-categories. arXiv:1705.07442, dec 2017. Google Scholar
  35. C. Sattler. The equivalence extension property and model structures. arXiv:1704.06911, 2017. Google Scholar
  36. M . Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, pages 1-86, 2017. Google Scholar
  37. B. Spitters. Cubical sets and the topological topos. arXiv:1610.05270, 2016. Google Scholar
  38. T. Uemura. Cubical assemblies and independence of the propositional resizing axiom. arXiv:1803.06649, apr 2018. Google Scholar
  39. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  40. V. Voevodsky. A simple type system with two identity types, 2013. URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf.
  41. V. Voevodsky. C-systems defined by universe categories: Presheaves. arXiv:1706.03620, jun 2017. Google Scholar
  42. D. Yetter. On right adjoints to exponentible functors. Journal of Pure and Applied Algebra, 45:287-304, 1987. Corrections in volume 58:103-105, 1989. 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 About DROPS Imprint Privacy Contact