← 返回首页
Internal Universes in Models of Homotopy Type Theory
Document

Internal Universes in Models of Homotopy Type Theory

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

PDF

File

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

Document Identifiers

Related Versions

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

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.

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

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.

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.
  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.
  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.
  10. L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory. Journal of Automated Reasoning, 2018.
  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.
  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.
  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.
  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).
  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.
  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.
  17. N. Gambino and C. Sattler. The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, 221:3027-3068, 2017.
  18. M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995.
  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.
  20. M. Hofmann and T. Streicher. Lifting Grothendieck universes. Unpublished note, 1999.
  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.
  22. C. Kapulkin and P. L. Lumsdaine. The simplicial model of univalent foundations (after Voedodsky). arXiv:1211.2851v4, jun 2016.
  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.
  24. F. W. Lawvere. Axiomatic cohesion. Theory and Applications of Categories, 19(3):41-49, 2007.
  25. Z. Luo. Notes on universes in type theory. Lecture notes for a talk at the Institute for Advanced Study, Princeton, 2012.
  26. S. MacLane. Categories for the Working Mathematician. Graduate Texts in Mathematics 5. Springer, 1971.
  27. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
  28. A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. ACM Trans. Comput. Logic, 9(3):23:1-23:49, 2008.
  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.
  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.
  31. I. Orton and A. M. Pitts. Decomposing the univalence axiom. arXiv:1712.04890, dec 2017.
  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].
  33. F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001.
  34. E. Riehl and M. Shulman. A type theory for synthetic ∞-categories. arXiv:1705.07442, dec 2017.
  35. C. Sattler. The equivalence extension property and model structures. arXiv:1704.06911, 2017.
  36. M . Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, pages 1-86, 2017.
  37. B. Spitters. Cubical sets and the topological topos. arXiv:1610.05270, 2016.
  38. T. Uemura. Cubical assemblies and independence of the propositional resizing axiom. arXiv:1803.06649, apr 2018.
  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.
  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.
Any Issues?
X

Feedback on the Current Page

Send
Submit

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing
OK

Could not send message

Please try again later or send an E-mail
OK
About DROPS

Schloss Dagstuhl - Leibniz Center for Informatics has been operating the Dagstuhl Research Online Publication Server (short: DROPS) since 2004. DROPS enables publication of the latest research findings in a fast, uncomplicated manner, in addition to providing unimpeded, open access to them. All the requisite metadata on each publication is administered in accordance with general guidelines pertaining to online publications (cf. Dublin Core). This enables the online publications to be authorized for citation and made accessible to a wide readership on a permanent basis. Access is free of charge for readers following the open access idea which fosters unimpeded access to scientific publications.

Instructions for Authors
Dagstuhl Series
Dagstuhl Journals
Instructions for Editors
Dagstuhl Series
Dagstuhl Journals
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact