nLab essentially small type

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}$$

See also

• type universe
• locally small type
• propositional resizing
• type theoretic axiom of replacement

References

• Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson: Section 2.19 of: Symmetry (2021) $[$pdf$]$