nLab global propositional resizing

Context

Universes

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

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 ii and jj, the type of propositions Prop i\mathrm{Prop}_i and Prop j\mathrm{Prop}_j of universes U iU_i and U jU_j are equivalent types. This implies that there is a type of all propositions Ω\Omega in some universe level which is equivalent to all Prop i\mathrm{Prop}_i. 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 Ω\Omega. If there is a base level 00 where 0i0 \leq i for all universe levels ii, then it is possible to assume global propositional resizing, that every U 0U_0-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 Ω\Omega in the type theory, there might be universes U iU_i which are predicative in the sense of not having the type of all propositions Ω\Omega. However, it suffices for impredicative mathematics to find a universe U iU_i which does contain the type of all propositions Ω\Omega.

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.

Definition

Using Russell universes

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 A:U iA:U_i to Lift i(A):U i+1\mathrm{Lift}_i(A):U_{i + 1} for all universe levels ii. The function λA:U i.Lift i(A):U iU i+1\lambda A:U_i.\mathrm{Lift}_i(A):U_i \to U_{i + 1} in U i+2U_{i + 2} restricts to a function

LiftProp i:( A:U iisProp(A) A:U i+1isProp(Lift i(A)))\mathrm{LiftProp}_i:\left(\sum_{A:U_i} \mathrm{isProp}(A) \to \sum_{A:U_{i+1}} \mathrm{isProp}(\mathrm{Lift}_i(A))\right)

in U i+2U_{i + 2} between the types of small propositions of the universes.

The axiom of global proposition resizing states that for all universe levels ii the function LiftProp i\mathrm{LiftProp}_i is an equivalence of types

ΓilevelΓglobalpropresize i:isEquiv(LiftProp i)\frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash \mathrm{globalpropresize}_i:\mathrm{isEquiv}(\mathrm{LiftProp}_i)}

The type of all propositions in the successor universe U i+1U_{i+1} may be resized to be equivalent to the type of all propositions in the smaller universe U iU_i. By the properties of equivalences one can show that the types of propositions of any two universes U iU_i and U jU_j are equivalent for any universe levels ii and jj, and that any such type of propositions is essentially U 1 U_1 -small.

The dependent type theory is then said to be globally impredicative. However, in the absence of local propositional resizing, the base universe U 0U_0 does not have an internal type of propositions.

Using Coquand universes

For general universe hierarchies

More generally, one can speak of global propositional resizing for universe hierarchies as actual structure in a dependent type theory.

Let (P,U,T,t)(P, U, T, t) be a hierarchy of weakly Tarski universes. By definition, PP is a preorder and there is a function

t: a:P b:P(ab)(U(a)U(b))t:\prod_{a:P} \prod_{b:P} (a \leq b) \to (U(a) \hookrightarrow U(b))

which states that for all terms a:Pa:P and b:Pb:P aba \leq b implies the type of embeddings U(a)U(b)U(a) \hookrightarrow U(b) is pointed. We thus have a natural map

t Ω: a:P b:P(ab)( A:U(a)isProp(T(a)(A)) A:U(b)isProp(T(b)(A)))t_\Omega:\prod_{a:P} \prod_{b:P} (a \leq b) \to \left(\sum_{A:U(a)} \mathrm{isProp}(T(a)(A)) \hookrightarrow \sum_{A:U(b)} \mathrm{isProp}(T(b)(A))\right)

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 a:Pa:P, b:Pb:P, and q:abq:a \leq b the embedding t Ω(a,b)(q)t_\Omega(a, b)(q) is an equivalence of types

globalpropresize: a:P b:P q:abisEquiv(t Ω(a,b)(q))\mathrm{globalpropresize}:\prod_{a:P} \prod_{b:P} \prod_{q:a \leq b} \mathrm{isEquiv}(t_\Omega(a, b)(q))

The type of all h-propositions in the larger universe U(a)U(a) may be resized to be equivalent to the type of all h-proposition in the smaller universe U(b)U(b).

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 U(a)U(a) indexed by a term a:Pa:P such that there is no element b:Pb:P where bab \leq a holds.

Usually, the hierarchy of Tarski universes is a sequential hierarchy indexed by the natural numbers N\mathrm{N}.

Created on August 20, 2024 at 14:39:48. See the history of this page for a list of all contributions to it.