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

TL;DR
This paper constructs a model of cubical type theory with a univalent, impredicative universe within cubical assemblies, demonstrating that propositional resizing fails in this setting.
Contribution
It introduces a novel cubical assembly model with a univalent, impredicative universe and shows the failure of propositional resizing within this framework.
Findings
Impredicative universe in the cubical assembly model does not satisfy propositional resizing.
The model demonstrates limitations of impredicative universes in cubical type theory.
Provides insights into the structure and constraints of cubical assemblies.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
