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
There are two definitions of an impredicative type universe in dependent type theory. Assuming that a type universe is closed under dependent sum types, dependent product types, and identity types/path types.
The first notion of impredicativity is propositional impredicativity, the notion that the type of small propositions in the universe is itself small. This is of the same strength as the existence of power sets in impredicative set theory, since power sets are represented by function sets into the resized type of all propositions in the universe.
The second notion of impredicativity is impredicative polymorphism, the notion that universal quantification of predicates over the universe in the universe are small. This, in the propositions as types interpretation, becomes that dependent product types of universe-indexed families of universe-small types are small.
Last revised on June 13, 2025 at 17:40:06. See the history of this page for a list of all contributions to it.