(in category theory/type theory/computer science)

**of all homotopy types**

**of (-1)-truncated types/h-propositions**

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

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

For a single universe $U$, propositional resizing states that the type of all h-propositions in a universe is essentially $U$-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}$

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

Last revised on November 27, 2023 at 16:43:58. See the history of this page for a list of all contributions to it.