(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, , we may define a type of mere propositions within that universe, . For universes, and , we have that entails . We thus have a natural map
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.
Last revised on June 16, 2022 at 09:50:54. See the history of this page for a list of all contributions to it.