nLab local 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, local propositional resizing is a weak version of the propositional resizing axiom which says that given a universe level ii, the type of propositions Prop i\mathrm{Prop}_i of each universe U iU_i is U iU_i-small. The dependent type theory is then said to be locally impredicative or to have local impredicativity.

Unlike the usual propositional resizing axiom, the local propositional resizing axiom makes no assumption on the equivalence of the types of propositions for different universe levels. It is possible to assume local propositional resizing, excluded middle for one universe U iU_i, and Brouwer's continuity principle for Dedekind real numbers for another universe U jU_j where j>ij \gt i, thus making Prop i\mathrm{Prop}_i and Prop j\mathrm{Prop}_j provably inequivalent types and contradicting the propositional resizing axiom.

Thus, while each universe U iU_i itself is impredicative in the sense of having a type of all U iU_i-small propositions, the dependent type theory itself is still predicative since there is no type of all propositions in the type theory. However, local propositional resizing suffices for impredicative mathematics in most cases, since one is usually working inside of a universe U iU_i and only the U iU_i-small propositions are relevant.

The name local propositional resizing and global propositional resizing, along with locally impredicative and globally impredicative is in analogue with local univalence and global univalence for univalent bicategories: while all univalent bicategories are locally univalent, not all locally univalent bicategories are univalent bicategories. Similarly, while all impredicative dependent type theories are locally impredicative, not all locally impredicative dependent type theories are impredicative.

Definition

We assume an infinite hierarchy of Russell universes or Coquand universes indexed by natural numbers in the metatheory or defined separately in some other sort.

The axiom of weak local propositional resizing says that the type of propositions A:U iisProp(A)\sum_{A:U_i} \mathrm{isProp}(A) is essentially U i U_i -small

ΓilevelΓpropresize i: Ω i:U iΩ i A:UisProp(A)\frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash \mathrm{propresize}_i:\sum_{\Omega_i:U_i} \Omega_i \simeq \sum_{A:U} \mathrm{isProp}(A)}

The dependent type theory is weakly locally impredicative or said to have weak local impredicativity.

The axiom of strict local propositional resizing says that the type of propositions A:U iisProp(A)\sum_{A:U_i} \mathrm{isProp}(A) is U iU_i-small:

ΓilevelΓΩ i:U iΓilevelΓΩ i A:U iisProp(A)\frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash \Omega_i:U_i} \qquad \frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash \Omega_i \equiv \sum_{A:U_i} \mathrm{isProp}(A)}

The dependent type theory is strictly locally impredicative or said to have strict local impredicativity.

In the case for Coquand universes, local propositional resizing is equivalent to saying that for each universe level ii one can construct a type of all propositions for the type judgment type i\mathrm{type}_i:

ΓilevelΓΩ itype i\frac{\Gamma \vdash i \mathrm{level}}{\Gamma \vdash \Omega_i \; \mathrm{type}_i}
ΓilevelΓAtype iΓtoProp i,A:isProp(A)Ω i\frac{\Gamma \vdash i \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i}{\Gamma \vdash \mathrm{toProp}_{i, A}:\mathrm{isProp}(A) \to \Omega_i}
ΓilevelΓA:Ω iΓEl i(A)type iΓilevelΓA:Ω iΓproptrunc i(A):isProp(El i(A))\frac{\Gamma \vdash i \mathrm{level} \quad \Gamma \vdash A:\Omega_i}{\Gamma \vdash \mathrm{El}_i(A) \; \mathrm{type}_i} \qquad \frac{\Gamma \vdash i \mathrm{level} \quad \Gamma \vdash A:\Omega_i}{\Gamma \vdash \mathrm{proptrunc}_i(A):\mathrm{isProp}(\mathrm{El}_i(A))}
ΓilevelΓAtype iΓp:isProp(A)ΓEl i(toProp i,A(p))Atype i\frac{\Gamma \vdash i \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{El}_i(\mathrm{toProp}_{i, A}(p)) \equiv A \; \mathrm{type}_i}
ΓilevelΓAtype iΓp:isProp(A)Γproptrunc i(toProp i,A(p))p:isProp(A)\frac{\Gamma \vdash i \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{proptrunc}_i(\mathrm{toProp}_{i, A}(p)) \equiv p:\mathrm{isProp}(A)}
ΓilevelΓA:Ω iΓAtoProp i,El i(A)(proptrunc i(A)):Ω i\frac{\Gamma \vdash i \mathrm{level} \quad \Gamma \vdash A:\Omega_i}{\Gamma \vdash A \equiv \mathrm{toProp}_{i, \mathrm{El}_i(A)}(\mathrm{proptrunc}_i(A)):\Omega_i}

For general universe hierarchies

More generally, one can speak of local propositional resizing of 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 local propositional resizing states that for all terms a:Pa:P there is a U(a)U(a)-small type Prop U(a)\mathrm{Prop}_{U(a)} which is equivalent to the type of all U(a)U(a)-small propositions.

localpropresize: a:P Ω U:U(a)T(Ω U) A:U(a)isProp(T(A))\mathrm{localpropresize}:\prod_{a:P} \sum_{\Omega_U:U(a)} T(\Omega_U) \simeq \sum_{A:U(a)} \mathrm{isProp}(T(A))

The universe hierarchy is then said to be locally impredicative. However, it may still be the case that the type of propositions for two universe are not equivalent to each other, meaning that the universe hierarchy itself is not impredicative.

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

Last revised on August 20, 2024 at 16:27:56. See the history of this page for a list of all contributions to it.