Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
arXiv:1803.06649 · doi: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.