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 mutually exclusive 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 closure under power sets, which in dependent type theory is represented by propositional resizing, 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.
Created on September 19, 2024 at 15:37:55. See the history of this page for a list of all contributions to it.