Contents

# Contents

## Definition

In dependent type theory, given a Russell universe $U$, a type $A$ is purely essentially $U$-small if the universe has an element $B:U$ and an equivalence $p:A \simeq B$.

A type $A$ is merely essentially $U$-small if there merely exists an element $B:U$ such that $A \simeq B$:

$\mathrm{isEssentiallySmall}_U(A) \coloneqq \exists B:U.A \simeq B$

Similarly, given a Tarski universe $(U, T)$, a type $A$ is purely essentially $U$-small if the universe has an element $B:U$ and an equivalence $p:A \simeq T(B)$.

A type $A$ is merely essentially $U$-small if there merely exists an element $B:U$ such that $A \simeq T(B)$:

$\mathrm{isEssentiallySmall}_U(A) \coloneqq \exists B:U.A \simeq T(B)$

## Examples

For a single universe $U$, propositional resizing states that the type of all h-propositions in a universe is essentially $U$-small.

## Making all essentially small types small

Given a Russell universe $U$, one could make all essentially $U$-small types actually small types by the following inference rules:

$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash \mathrm{witnSmall}_A:\exists B:U.A \simeq B}{\Gamma \vdash A:U}$