Document Open Access Logo

Decomposing the Univalence Axiom

Authors Ian Orton , Andrew M. Pitts

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2017.6.pdf
  • Filesize: 0.52 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • dependent type theory
  • homotopy type theory
  • univalent type theory
  • univalence
  • cubical type theory
  • cubical sets

Metrics

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

Abstract

This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.

Cite As Get BibTex

Ian Orton and Andrew M. Pitts. Decomposing the Univalence Axiom. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.TYPES.2017.6

Author Details

Ian Orton
  • University of Cambridge Dept. Computer Science & Technology, Cambridge, UK
Andrew M. Pitts
  • University of Cambridge Dept. Computer Science & Technology, Cambridge, UK

Funding

  • Orton, Ian: Supported by a UK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.

Supplementary Materials

References

  1. Agda Project. URL: http://wiki.portal.chalmers.se/agda.
  2. C. Angiuli, G. Brunerie, T. Coquand, K.-B. Hou (Favonia), R. Harper, and D. R. Licata. Cartesian Cubical Type Theory (preprint), 2017. URL: https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf.
  3. S. Awodey. A cubical model of homotopy type theory. arXiv preprint arXiv:1607.06413, 2016. URL: https://arxiv.org/abs/1607.06413.
  4. R. Balbes and P. Dwinger. Distributive Lattices. University of Missouri Press, 1975. Google Scholar
  5. 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, pages 107-128, 2014. Google Scholar
  6. L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:17, 2016. Google Scholar
  7. A. B. Booij, M. H. Escardó, P. L. Lumsdaine, and M. Shulman. Parametricity, automorphisms of the universe, and excluded middle. arXiv preprint arXiv:1701.05617, 2017. URL: https://arxiv.org/abs/1701.05617.
  8. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 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, 2018. Google Scholar
  9. 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
  10. 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
  11. M. Hofmann and T. Streicher. Lifting Grothendieck Universes (Unpublished note), 1997. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  12. 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
  13. 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. URL: https://arxiv.org/abs/1712.04864.
  14. A. M. Pitts. Nominal Presentation of Cubical Sets Models of Type Theory. In LIPIcs-Leibniz International Proceedings in Informatics, volume 39. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  15. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. Univalent Foundations Project, Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact