(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 homotopy type theory, given a type universe $\mathcal{U}$, a type $A$ is **locally $\mathcal{U}$-small** if for all terms $a:A$ and $b:A$, the identity type $a =_A b$ is essentially $\mathcal{U}$-small.

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

Last revised on June 16, 2022 at 13:58:52. See the history of this page for a list of all contributions to it.