Internal Universes in Models of Homotopy Type Theory
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.
cubical sets
dependent type theory
homotopy type theory
internal language
modalities
univalent foundations
universes
Theory of computation~Type theory
22:1-22:17
Regular Paper
https://doi.org/10.17863/CAM.22369 (Agda-flat source code)
https://arxiv.org/abs/1801.07664
Daniel R.
Licata
Daniel R. Licata
Wesleyan University Dept. Mathematics & Computer Science, Middletown, USA
https://orcid.org/0000-0003-0697-7405
Supported by United States Air Force Research Laboratory, agreement numbers FA-95501210370 and FA-95501510053.
Ian
Orton
Ian Orton
University of Cambridge Dept. Computer Science & Technology, Cambridge, UK
https://orcid.org/0000-0002-9924-0623
Supported by a UK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.
Andrew M.
Pitts
Andrew M. Pitts
University of Cambridge Dept. Computer Science & Technology, Cambridge, UK
https://orcid.org/0000-0001-7775-3471
Bas
Spitters
Bas Spitters
Aarhus University Dept. Computer Science, Aarhus, DK
https://orcid.org/0000-0002-2802-0973
Supported by the Guarded Homotopy Type Theory project, funded by the Villum Foundation, project number 12386.
10.4230/LIPIcs.FSCD.2018.22
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.
Agda-flat. URL: https://github.com/agda/agda/tree/flat.
https://github.com/agda/agda/tree/flat
Agda Project. URL: https://wiki.portal.chalmers.se/agda.
https://wiki.portal.chalmers.se/agda
T. Altenkirch, P. Capriotti, and N. Kraus. Extending homotopy type theory with strict equality, 2016. URL: http://arxiv.org/abs/1604.03799.
http://arxiv.org/abs/1604.03799
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.
https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf
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.
http://arxiv.org/abs/1712.01800
S. Awodey. Notes on cubical models of type theory, 2016. URL: https://github.com/awodey/math/blob/master/Cubical/cubical.pdf.
https://github.com/awodey/math/blob/master/Cubical/cubical.pdf
R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, 1975.
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.
L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory. Journal of Automated Reasoning, 2018.
U. Buchholtz and E. Morehouse. Varieties of cubical sets. In Relational and Algebraic Methods in Computer Science: 16th International Conference (RAMiCS 2017), Proceedings, 2017.
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.
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.
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).
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.
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.
N. Gambino and C. Sattler. The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, 221:3027-3068, 2017.
M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995.
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.
M. Hofmann and T. Streicher. Lifting Grothendieck universes. Unpublished note, 1999.
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.
C. Kapulkin and P. L. Lumsdaine. The simplicial model of univalent foundations (after Voedodsky). arXiv:1211.2851v4, jun 2016.
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.
F. W. Lawvere. Axiomatic cohesion. Theory and Applications of Categories, 19(3):41-49, 2007.
Z. Luo. Notes on universes in type theory. Lecture notes for a talk at the Institute for Advanced Study, Princeton, 2012.
S. MacLane. Categories for the Working Mathematician. Graduate Texts in Mathematics 5. Springer, 1971.
P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. ACM Trans. Comput. Logic, 9(3):23:1-23:49, 2008.
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.
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.
I. Orton and A. M. Pitts. Decomposing the univalence axiom. arXiv:1712.04890, dec 2017.
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].
F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001.
E. Riehl and M. Shulman. A type theory for synthetic ∞-categories. arXiv:1705.07442, dec 2017.
C. Sattler. The equivalence extension property and model structures. arXiv:1704.06911, 2017.
M . Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, pages 1-86, 2017.
B. Spitters. Cubical sets and the topological topos. arXiv:1610.05270, 2016.
T. Uemura. Cubical assemblies and independence of the propositional resizing axiom. arXiv:1803.06649, apr 2018.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
http://homotopytypetheory.org/book
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.
https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf
V. Voevodsky. C-systems defined by universe categories: Presheaves. arXiv:1706.03620, jun 2017.
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.
Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode