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

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.