nLab propositional resizing

Idea

Propositional resizing is an axiom often assumed in homotopy type theory that states that all mere propositions are small. This is a form of impredicativity: without it, no universes can be shown to be closed under forming power sets.

Propositional resizing is a relatively weak axiom, for instance it is implied by the law of excluded middle, which states that the small type $2$ classifies all propositions. However, it is independent of the other basic axioms of homotopy type theory.

Definition

A universe $\mathcal{V}$ satisfies $\mathcal{U}$-propositional resizing if every $\mathcal{V}$ proposition is essentially $\mathcal{U}$-small. Propositional resizing is then the axiom that all universes $\mathcal{V}$ satisfy $\mathcal{U}$ resizing for all universes $\mathcal{U}$.

If $\mathcal{V}$ contains a type classifying all $\mathcal{U}$ types, then the type $Prop_{\mathcal{U}}$ is a $\mathcal{V}$-small type of all $\mathcal{V}$ propositions, making $\mathcal{V}$ an impredicative universe.

See also

• essentially small type

• excluded middle

• type of all propositions

• impredicative dependent type theory

• impredicative universe

References

• Section 3.5 of The HoTT Book

• Taichi Uemura, Cubical Assemblies and the Independence of the Propositional Resizing Axiom, HoTT/UF 2018 abstract slides

• Formalization in Agda Unimath.