Contents

# Contents

## Definition

In homotopy type theory, given a type universe $\mathcal{U}$, a type $A$ is essentially $\mathcal{U}$-small if there purely is a term $B:\mathcal{U}$ and an equivalence $p:A \cong B$.

## Examples

The axiom of propositional resizing states that all propositions are essentially small relative to the smallest universe in the universe hierarchy.