Document Open Access Logo

Axioms for Modelling Cubical Type Theory in a Topos

Authors Ian Orton, Andrew M. Pitts

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.24.pdf
  • Filesize: 0.55 MB
  • 19 pages

Document Identifiers

Author Details

Ian Orton
Andrew M. Pitts

Cite AsGet BibTex

Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CSL.2016.24

Abstract

The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model of type theory in which elements of identity types are functions with domain I. Cohen, Coquand, Huber and Mörtberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style.
Keywords
  • models of dependent type theory
  • homotopy type theory
  • cubical sets
  • cubical type theory
  • topos
  • univalence

Metrics

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

References

  1. P. Aczel and M. Rathjen. Notes on constructive set theory. Book draft, 2010. Google Scholar
  2. J. Adámek, J. Rosický, and E. M. Vitale. Algebraic Theories: a Categorical Introduction to General Algebra, volume 184 of Cambridge Tracts in Mathematics. Cambridge University Press, 2010. Google Scholar
  3. Agda Project. URL: http://wiki.portal.chalmers.se/agda.
  4. S. Awodey. Natural models of homotopy type theory. ArXiv e-prints, arXiv:1406.3219v2 [math.CT], March 2015. Google Scholar
  5. R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, 1975. Google Scholar
  6. M. Bezem and T. Coquand. A Kripke model for simplicial sets. Theoretical Computer Science, 574:86-91, 2015. Google Scholar
  7. M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets. In R. Matthes and A. Schubert, editors, Proc. TYPES 2013, volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107-128. Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  8. L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Verozzi. Guarded cubical type theory. Abstract of a talk at TYPES 2016, Novi Sad, Serbia, 2016. Google Scholar
  9. R. Brown and G. H. Mosa. Double categories, 2-categories, thin structures and connections. Theory and Applications of Categories, 5(7):163-175, 1999. Google Scholar
  10. J. Cockx and A. Abel. Sprinkles of extensionality for your vanilla type theory. Abstract of a talk at TYPES 2016, Novi Sad, Serbia, 2016. Google Scholar
  11. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Preprint, December 2015. Google Scholar
  12. T. Coquand. A cubical type theory, August 2015. Slides of an invited talk at Domains XII, University of Cork, Ireland, URL: https://www.cse.chalmers.se/~coquand/cork.pdf.
  13. T. Coquand and N. A. Danielsson. Isomorphism is equality. Indagationes Mathematicae, 24(4):1105-1120, 2013. Google Scholar
  14. 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
  15. M. Escardo. A small type of propositions à la in Agda, August 2015. URL: http://www.cs.bham.ac.uk/~mhe/impredicativity/.
  16. P. Gabriel and F. Ulmer. Lokal Präsentierbare Kategorien, volume 221 of Lecture Notes in Mathematics. Springer-Verlag, 1971. Google Scholar
  17. N. Gambino and C. Sattler. Uniform Fibrations and the Frobenius Condition. ArXiv e-prints, arXiv:1510.00669, October 2015. Google Scholar
  18. P. G. Goerss and J. F. Jardine. Simplicial Homotopy Theory. Modern Birkhäuser Classics. Birkhäuser Basel, 2009. 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. S. Huber. A Model of Type Theory in Cubical Sets. Licentiate thesis, University of Gothenburg, May 2015. Google Scholar
  22. P. T. Johnstone. On a topological topos. Proceedings of the London Mathematical Society, s3-38(2):237-271, 1979. Google Scholar
  23. C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. arXiv preprint, arXiv:1211.2851v2 [math.LO], April 2014. Google Scholar
  24. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986. Google Scholar
  25. F. W. Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(1):869-872, 1963. Google Scholar
  26. P. L. Lumsdaine and M. A. Warren. The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Logic, 16(3):23:1-23:31, July 2015. Google Scholar
  27. M. E. Maietti. Modular correspondence between dependent type theories and categories including pretopoi and topoi. Mathematical Structures in Computer Science, 15:1089-1149, 2005. Google Scholar
  28. P. J. May. A Concise Course in Algebraic Topology. Chicago Lectures in Mathematics. University of Chicago Press, 1999. Google Scholar
  29. A. M. Pitts. Categorical logic. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, pages 40-128. Oxford University Press, 2000. Google Scholar
  30. A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  31. B. Spitters. Cubical sets as a classifying topos. Abstract of a talk at TYPES 2015, Tallinn, Estonia, 2015. Google Scholar
  32. A. Swan. An algebraic weak factorisation system on 01-substitution sets: A constructive proof. ArXiv e-prints, arXiv:1409.1829, September 2014. URL: http://arxiv.org/abs/1409.1829.
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
  34. B. van den Berg. Path categories and propositional identity types. ArXiv e-prints, arXiv:1604.06001 [math.CT], April 2016. 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