(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 dependent type theory defined via universes and universe levels, global propositional resizing is a weak version of the propositional resizing axiom which says that given two universe levels and , the type of propositions and of universes and are equivalent types. This implies that there is a type of all propositions in some universe level which is equivalent to all . The dependent type theory is then said to be globally impredicative or have global impredicativity.
Unlike the usual propositional resizing axiom, the global propositional resizing axiom makes no assumption on whether all universes contain . If there is a base level where for all universe levels , then it is possible to assume global propositional resizing, that every -small type has a tight apartness relation, and Brouwer's continuity principle for the Dedekind real numbers, contradicting the propositional resizing axiom.
Thus, while the dependent type theory itself is impredicative since there is a type of all propositions in the type theory, there might be universes which are predicative in the sense of not having the type of all propositions . However, it suffices for impredicative mathematics to find a universe which does contain the type of all propositions .
The names global propositional resizing and local propositional resizing, along with globally impredicative and locally impredicative is in analogue with global univalence and local univalence for univalent bicategories: while all univalent bicategories are globally univalent, not all globally univalent bicategories are univalent bicategories. Similarly, while all impredicative dependent type theories are globally impredicative, not all globally impredicative dependent type theories are impredicative.
We assume an infinite hierarchy of Russell universes indexed by natural numbers in the metatheory or defined separately in some other sort. The Russell universes are non-cumulative in the sense that there is a lifting operation which takes types to for all universe levels . The function in restricts to a function
in between the types of small propositions of the universes.
The axiom of global proposition resizing states that for all universe levels the function is an equivalence of types
The type of all propositions in the successor universe may be resized to be equivalent to the type of all propositions in the smaller universe . By the properties of equivalences one can show that the types of propositions of any two universes and are equivalent for any universe levels and , and that any such type of propositions is essentially -small.
The dependent type theory is then said to be globally impredicative. However, in the absence of local propositional resizing, the base universe does not have an internal type of propositions.
…
More generally, one can speak of global propositional resizing for universe hierarchies as actual structure in a dependent type theory.
Let be a hierarchy of weakly Tarski universes. By definition, is a preorder and there is a function
which states that for all terms and implies the type of embeddings is pointed. We thus have a natural map
which is the restriction of the above function to small propositions of the universe.
The axiom of global proposition resizing for the universe hierarchy states that for all terms , , and the embedding is an equivalence of types
The type of all h-propositions in the larger universe may be resized to be equivalent to the type of all h-proposition in the smaller universe .
The universe hierarchy is then said to be globally impredicative. However, it may still be the case that there are universes which do not have an internal type of propositions, such as, in the absence of local propositional resizing, any universe indexed by a term such that there is no element where holds.
Usually, the hierarchy of Tarski universes is a sequential hierarchy indexed by the natural numbers .
Created on August 20, 2024 at 14:39:48. See the history of this page for a list of all contributions to it.