Document Open Access Logo

Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing

Author Taichi Uemura

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2018.7.pdf
  • Filesize: 0.54 MB
  • 20 pages

Document Identifiers

Author Details

Taichi Uemura
  • University of Amsterdam, Amsterdam, The Netherlands

Funding

This work is part of the research programme "The Computational Content of Homotopy Type Theory" with project number 613.001.602, which is financed by the Netherlands Organisation for Scientific Research (NWO).

Acknowledgements

I would like to thank Benno van den Berg, Martijn den Besten and Andrew Swan for helpful discussions and comments, and Bas Spitters, Steve Awodey and the anonymous reviewer for their comments, questions and suggestions.

Cite AsGet BibTex

Taichi Uemura. Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.TYPES.2018.7

Abstract

We construct a model of cubical type theory with a univalent and impredicative universe in a category of cubical assemblies. We show that this impredicative universe in the cubical assembly model does not satisfy a form of propositional resizing.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Denotational semantics
Keywords
  • Cubical type theory
  • Realizability
  • Impredicative universe
  • Univalence
  • Propositional resizing

Metrics

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

References

  1. Steve Awodey. Impredicative encodings in HoTT, 2017. Talk at the workshop "Computer-aided mathematical proof". URL: http://www.newton.ac.uk/seminar/20170711090010001.
  2. Steve Awodey, Jonas Frey, and Sam Speight. Impredicative Encodings of (Higher) Inductive Types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 76-85, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3209108.3209130.
  3. Steven Awodey and Andrej Bauer. Propositions As [Types]. J. Log. and Comput., 14(4):447-471, August 2004. URL: https://doi.org/10.1093/logcom/14.4.447.
  4. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT Library: A Formalization of Homotopy Type Theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 164-172, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3018610.3018615.
  5. Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In Ralph Matthes and Aleksy Schubert, editors, 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107-128, Dagstuhl, Germany, 2014. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2013.107.
  6. Marc Bezem, Thierry Coquand, and Simon Huber. The Univalence Axiom in Cubical Sets. Journal of Automated Reasoning, 63(2):159-171, August 2019. URL: https://doi.org/10.1007/s10817-018-9472-6.
  7. Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, and Bas Spitters. Modal Dependent Type Theory and Dependent Right Adjoints, 2019. URL: http://arxiv.org/abs/1804.05236v3.
  8. Ulrik Buchholtz and Edward Morehouse. Varieties of Cubical Sets. In Peter Höfner, Damien Pous, and Georg Struth, editors, Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings, pages 77-92. Springer International Publishing, Cham, 2017. URL: https://doi.org/10.1007/978-3-319-57418-9_5.
  9. J.W. Cartmell. Generalised algebraic theories and contextual categories. PhD thesis, Oxford University, 1978. Google Scholar
  10. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo 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. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  11. Thierry Coquand. Internal version of the uniform Kan filling condition, 2015. URL: http://www.cse.chalmers.se/~coquand/shape.pdf.
  12. 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, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3209108.3209197.
  13. Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  14. Peter Dybjer. Internal Type Theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs: International Workshop, TYPES '95 Torino, Italy, June 5-8, 1995 Selected Papers, pages 120-134. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61780-9_66.
  15. Jonas Frey. Towards a realizability model of homotopy type theory, 2017. Talk at CT 2017. URL: http://www.mat.uc.pt/~ct2017/slides/frey_j.pdf.
  16. Dan Frumin and Benno van den Berg. A homotopy-theoretic model of function extensionality in the effective topos. Mathematical Structures in Computer Science, pages 1-27, 2018. URL: https://doi.org/10.1017/S0960129518000142.
  17. 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.
  18. Richard Garner. Understanding the Small Object Argument. Applied Categorical Structures, 17(3):247-285, June 2009. URL: https://doi.org/10.1007/s10485-008-9137-4.
  19. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. URL: http://www.paultaylor.eu/stable/Proofs+Types.html.
  20. Martin Hofmann and Thomas Streicher. Lifting Grothendieck Universes, 1997. URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  21. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83-111. Oxford Univ. Press, New York, 1998. Google Scholar
  22. J.M.E. Hyland. The Effective Topos. In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 165-216. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70129-6.
  23. J.M.E. Hyland. A small complete category. Annals of Pure and Applied Logic, 40(2):135-165, 1988. URL: https://doi.org/10.1016/0168-0072(88)90018-8.
  24. Bart Jacobs. Comprehension categories and the semantics of type dependency. Theoretical Computer Science, 107(2):169-207, 1993. URL: https://doi.org/10.1016/0304-3975(93)90169-T.
  25. Bart Jacobs. Categorical Logic and Type Theory. Elsevier Science, 1st edition, 1999. Google Scholar
  26. Chris Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky), 2018. URL: http://arxiv.org/abs/1211.2851v5.
  27. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  28. Giuseppe Longo and Eugenio Moggi. Constructive natural deduction and its "ω-set" interpretation. Mathematical Structures in Computer Science, 1(2):215-254, 1991. URL: https://doi.org/10.1017/S0960129500001298.
  29. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. Studies in Logic and the Foundations of Mathematics, 80:73-118, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  30. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:19, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.24.
  31. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, 14, December 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  32. Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, The University of Edinburgh, 2006. URL: http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/.
  33. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study, 2013.
  34. Christian Sattler. The Equivalence Extension Property and Model Structures, 2017. URL: http://arxiv.org/abs/1704.06911v4.
  35. Michael Shulman. Higher Inductive Types via Impredicative Polymorphism, 2011. URL: https://homotopytypetheory.org/2011/04/25/higher-inductive-types-via-impredicative-polymorphism/.
  36. Sam Speight. Impredicative Encodings of Inductive Types in Homotopy Type Theory. Master’s thesis, Carnegie Mellon University, 2017. URL: http://www.cs.ox.ac.uk/people/sam.speight/publications/sams-hott-thesis.pdf.
  37. Bas Spitters. Cubical sets and the topological topos, 2016. URL: http://arxiv.org/abs/1610.05270v1.
  38. Wouter Pieter Stekelenburg. Constructive Simplicial Homotopy, 2016. URL: http://arxiv.org/abs/1604.04746v1.
  39. Andrew W. Swan. An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof. Journal of Logic &Analysis, 8:1-35, 2016. URL: https://doi.org/10.4115/jla.2016.8.1.
  40. Andrew W. Swan. Lifting Problems in Grothendieck Fibrations, 2018. URL: http://arxiv.org/abs/1802.06718v1.
  41. Andrew W. Swan. W-Types with Reductions and the Small Object Argument, 2018. URL: http://arxiv.org/abs/1802.07588v1.
  42. Andrew W. Swan and Taichi Uemura. On Church’s Thesis in Cubical Assemblies, 2019. URL: http://arxiv.org/abs/1905.03014v1.
  43. Benno van den Berg. Univalent polymorphism, 2018. URL: http://arxiv.org/abs/1803.10113v2.
  44. Jaap van Oosten. Realizability: An Introduction to Its Categorical Side, volume 152 of Studies in Logic and the Foundations of Mathematics. Elsevier Science, San Diego, USA, 2008. Google Scholar
  45. Vladimir Voevodsky. A universe polymorphic type system, 2012. URL: https://ncatlab.org/ufias2012/files/Universe+polymorphic+type+sytem.pdf.
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