resizing axiom

(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 formal logic and specifically in type theory, a *resizing rule* is an introduction rule which allows, under suitable conditions, to find a type that is in some type universe $U_2$ also in a smaller type universe $U_1$.

- Vladimir Voevodsky,
*Resizing Rules - their use and semantic*justification_, 2011 (pdf)

Last revised on March 26, 2015 at 19:18:16. See the history of this page for a list of all contributions to it.