propositional resizing

(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 universe, $\mathcal{U}$, we may define a type of mere propositions within that universe, $\sum_{A: \mathcal{U}} isProp(A)$. For universes, $\mathcal{U}_i$ and $\mathcal{U}_{i+1}$, we have that $A: \mathcal{U}_i$ entails $A:\mathcal{U}_{i+1}$. We thus have a natural map

$Prop_{\mathcal{U}_i} \to Prop_{\mathcal{U}_{i+1}}.$

The axiom of **proposition resizing** states that this map is an equivalence. Any mere proposition in the larger universe may be *resized* to an equivalent mere proposition in the smaller universe.

The axiom is a form of impredicativity for mere propositions, and by avoiding its use, the type theory is said to remain predicative.

- Section 3.5 of The HoTT Book

Created on September 24, 2018 at 06:45:28. See the history of this page for a list of all contributions to it.