Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
- Uemura, Taichi
Publication date
January 2019
DOI Publisher
LIPIcs - Leibniz International Proceedings in Informatics. 24th International Conference on Types for Proofs and Programs (TYPES 2018)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
Add to ORKG