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

Open Access
Authors
Publication date 11-2019
Host editors
  • P. Dybjer
  • J. Espírito Santo
  • L. Pinto
Book title 24th International Conference on Types for Proofs and Programs
Book subtitle TYPES 2018, June 18-21, 2018, Braga, Portugal
ISBN (electronic)
  • 9783959771061
Series Leibniz International Proceedings in Informatics
Event 24th International Conference on Types for Proofs and Programs
Article number 7
Number of pages 20
Publisher Saarbrücken/Wadern: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Organisations
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
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.
Document type Conference contribution
Language English
Published at https://doi.org/10.4230/LIPIcs.TYPES.2018.7
Other links https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16128
Downloads
LIPIcs-TYPES-2018-7 (Final published version)
Permalink to this page
Back