Document Open Access Logo

Unifying Cubical Models of Univalent Type Theory

Authors Evan Cavallo , Anders Mörtberg, Andrew W Swan

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.14.pdf
  • Filesize: 0.5 MB
  • 17 pages

Document Identifiers

Author Details

Evan Cavallo
  • School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
Anders Mörtberg
  • School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA
  • Department of Mathematics, Stockholm University, Sweden
Andrew W Swan
  • Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands

Funding

  • Cavallo, Evan: This author was supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the AFOSR.

Acknowledgements

We are grateful to Carlo Angiuli, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, Daniel R. Licata, Andrew Pitts and Jon Sterling for helpful comments and remarks on earlier versions of this work. The first two authors are also thankful to Mathieu Anel and Steve Awodey for their illuminating lectures on homotopical algebra in the CMU HoTT seminar.

Cite As Get BibTex

Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.14

Abstract

We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Cubical Set Models
  • Cubical Type Theory
  • Homotopy Type Theory
  • Univalent Foundations

Metrics

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

References

  1. Agda development team. Agda 2.6.0.1 documentation, 2018. URL: https://agda.readthedocs.io/en/v2.6.0.1/.
  2. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. Syntax and Models of Cartesian Cubical Type Theory. Draft available at https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf, 2017.
  3. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 6:1-6:17, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.6.
  4. Steve Awodey. A cubical model of homotopy type theory. Annals of Pure and Applied Logic, 169(12):1270-1294, 2018. Logic Colloquium 2015. URL: https://doi.org/10.1016/j.apal.2018.08.002.
  5. Steve Awodey. Recent Work in Homotopy Type Theory: Modal, Algebraic, Synthetic, and Cubical, March 2018. Talk given at MURI Team Meeting at CMU, available at URL: https://ncatlab.org/homotopytypetheory/files/awodeyMURI18.pdf.
  6. Steve Awodey. A Quillen model structure on the category of cartesian cubical sets. Preprint available at https://github.com/awodey/math/blob/master/QMS/qms.pdf, 2019.
  7. Marc Bezem, Thierry Coquand, and Simon 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. URL: https://doi.org/10.4230/LIPIcs.TYPES.2013.107.
  8. Marc Bezem, Thierry Coquand, and Simon Huber. The Univalence Axiom in Cubical Sets. J. Autom. Reasoning, 63(2):159-171, 2019. URL: https://doi.org/10.1007/s10817-018-9472-6.
  9. Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 92-106, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.92.
  10. Simon Boulier. Extending Type Theory with Syntactic Models. PhD thesis, Université Bretagne Loire, 2018. Google Scholar
  11. Evan Cavallo. Stable factorization from a fibred algebraic weak factorization system. Preprint arXiv:1910.03121 [math.CT], 2019. Google Scholar
  12. Evan Cavallo and Robert Harper. Higher Inductive Types in Cubical Computational Type Theory. Proc. ACM Program. Lang., 3(POPL):1:1-1:27, January 2019. URL: https://doi.org/10.1145/3290314.
  13. Evan Cavallo and Anders Mörtberg. A Unifying Cartesian Cubical Type Theory. Preprint available at https://github.com/mortberg/gen-cart/blob/master/unifying-cartesian.pdf, 2019.
  14. Evan Cavallo, Anders Mörtberg, and Andrew Swan. Model Structures on Cubical Sets. Preprint available at https://github.com/mortberg/gen-cart/blob/master/modelstructure.pdf, 2019.
  15. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Types for Proofs and Programs (TYPES 2015), volume 69 of LIPIcs, pages 5:1-5:34, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  16. Thierry Coquand. Variation on cubical sets. Unpublished note available at https://www.cse.chalmers.se/~coquand/diag1.pdf, 2014.
  17. Thierry Coquand. Quillen model structure. Link and discussion available at https://groups.google.com/forum/#!msg/homotopytypetheory/RQkLWZ_83kQ/tAyb3zYTBQAJ, 2018.
  18. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  19. Thierry Coquand, Simon Huber, and Christian Sattler. Homotopy Canonicity for Cubical Type Theory. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., volume 131 of LIPIcs, pages 11:1-11:23. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.11.
  20. Albrecht Dold and Rene Thom. Quasifaserungen und Unendliche Symmetrische Produkte. Annals of Mathematics, 67(2):239-281, 1958. URL: https://doi.org/10.2307/1970005.
  21. Peter Dybjer. Internal Type Theory. In Lecture Notes in Computer Science, pages 120-134. Springer Verlag, Berlin, Heidelberg, New York, 1996. URL: https://doi.org/10.1007/3-540-61780-9_66.
  22. Dan Frumin and Benno Van den Berg. A homotopy-theoretic model of function extensionality in the effective topos. Mathematical Structures in Computer Science, 29(4):588–614, 2019. URL: https://doi.org/10.1017/S0960129518000142.
  23. Nicola Gambino and Simon Henry. Towards a constructive simplicial model of Univalent Foundations. Preprint arXiv:1905.06281 [math.CT], 2019. Google Scholar
  24. Nicola Gambino and Christian Sattler. The Frobenius condition, right properness, and uniform fibrations. Journal of Pure and Applied Algebra, 221(12):3027-3068, 2017. URL: https://doi.org/10.1016/j.jpaa.2017.02.013.
  25. Martin Hofmann. Syntax and semantics of dependent types. In A.M. Pitts and P. Dybjer, editors, Semantics and logics of computation, volume 14 of Publ. Newton Inst., pages 79-130. Cambridge University Press, Cambridge, 1997. Papers from the Summer School held at the University of Cambridge, Cambridge, September 1995. URL: https://doi.org/10.1017/CBO9780511526619.004.
  26. Chris Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky). Preprint arXiv:1211.2851v4 [math.LO], November 2012. Google Scholar
  27. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In FSCD, volume 108 of LIPIcs, pages 22:1-22:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  28. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, Volume 14, Issue 4, December 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  29. Jason Parker. Duality between Cubes and Bipointed Sets. Master’s thesis, Carnegie Mellon University, 2014. Google Scholar
  30. C. L. Reedy. Homotopy Theory of Model Categories. Unpublished note available at http://www-math.mit.edu/~psh/reedy.pdf, 1974.
  31. Emily Riehl. Categorical Homotopy Theory. New Mathematical Monographs. Cambridge University Press, 2014. URL: https://doi.org/10.1017/CBO9781107261457.
  32. Christian Sattler. The Equivalence Extension Property and Model Structures. Preprint arXiv:1704.06911v1 [math.CT], 2017. Google Scholar
  33. Andrew Swan. Identity Types in Algebraic Model Structures and Cubical Sets. Preprint arXiv:1808.00915 [math.CT], August 2018. Google Scholar
  34. Andrew Swan. Lifting Problems in Grothendieck Fibrations. Preprint arXiv:1802.06718 [math.CT], February 2018. Google Scholar
  35. Andrew Swan. Separating Path and Identity Types in Presheaf Models of Univalent Type Theory. Preprint arXiv:1808.00920 [math.LO], 2018. Google Scholar
  36. Andrew Swan. W-types with reductions and the small object argument. Preprint arXiv:1802.07588 [math.CT], February 2018. Google Scholar
  37. Taichi Uemura. Cubical Assemblies and Independence of the Propositional Resizing Axiom. Preprint arXiv:1803.06649 [cs.LO], 2018. Google Scholar
  38. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  39. Vladimir Voevodsky. An experimental library of formalized Mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25:1278-1294, 2015. URL: https://doi.org/10.1017/S0960129514000577.
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