nLab propositional resizing

Contents

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 set theory/category theory

In a constructive weakly predicative structural set theory, such as doing mathematics in a well-pointed cartesian closed lextensive coherent category with a natural numbers object, it is still possible to define a category inside of the set theory, and in particular, it is still possible to define a well-pointed cartesian closed lextensive coherent category object with a natural numbers object inside of any well-pointed cartesian closed lextensive coherent category with a natural numbers object. These objects are called universes or Grothendieck universes 𝒰\mathcal{U} in structural set theory. From here, one could form the sub-(0,1)-category of subterminal objects Ω 𝒰\Omega_\mathcal{U} in 𝒰\mathcal{U}, the set of 𝒰\mathcal{U}-small subsingletons, and subsingletons model propositions in the universe, so could be called a set of 𝒰\mathcal{U}-small propositions as well.

If a set theory has multiple such universes 𝒰\mathcal{U} and 𝒱\mathcal{V}, then there are multiple such sets of propositions, one of which is 𝒰\mathcal{U}-small, and another one of which is 𝒱\mathcal{V}-small. In general, the set of 𝒰\mathcal{U}-small propositions Ω 𝒰\Omega_\mathcal{U} and the set of 𝒱\mathcal{V}-small propositions Ω 𝒱\Omega_\mathcal{V} cannot be proven to be equivalent to each other. However, propositional resizing is the axiom that for universe 𝒰\mathcal{U} and 𝒱\mathcal{V}, the set of 𝒰\mathcal{U}-small propositions is in bijection with the set of 𝒱\mathcal{V}-small propositions, Ω 𝒰Ω 𝒱\Omega_\mathcal{U} \cong \Omega_\mathcal{V}.

In type theory

In homotopy type theory, the type of h-propositions of a Tarski universe (or Russell universe) UU is not in general essentially U U -small. Propositional resizing is then the statement that the type of h-propositions is essentially UU-small.

There is a separate axiom of propositional resizing for a hierarchy of universes, where the type of h-propositions of each universe, where one universe embeds into the other universe, are equivalent to each other.

Propositional resizing is a form of impredicativity for h-propositions, and by avoiding its use, the universe or hierarchy is said to remain predicative.

However, when using Tarski universes, while universes and universe hierarchies may be impredicative, the overarching type theory is still predicative if it has a judgment ‘AtypeA \; \mathrm{type}’, since it is impossible to talk about all types.

Definition

In set theory/category theory

We work in a structural set theory which externally forms a well-pointed cartesian closed lextensive coherent category with a natural numbers object, namely a structural set theory with

Any well-pointed cartesian closed coherent category with a natural numbers object inside of the set theory is thus an internal model of the set theory, and thus could be considered to be a universe inside of the set theory.

In type theory

For individual universes

Let (U,T)(U, T) be a weakly Tarski universe and let

A:UisProp(T(A))\sum_{A:U} \mathrm{isProp}(T(A))

be the type of all propositions in UU. The weakly Tarski universe (U,T)(U, T) is impredicative or satisfies propositional resizing if it has a term Ω U:U\Omega_U:U and an equivalence

propresize:T(Ω U) A:UisProp(T(A))\mathrm{propresize}:T(\Omega_U) \simeq \sum_{A:U} \mathrm{isProp}(T(A))

A weakly Tarski universe is strictly impredicative or satisfies strict propositional resizing if the above equivalence becomes a definitional equality:

T(Ω U) A:UisProp(T(A))T(\Omega_U) \equiv \sum_{A:U} \mathrm{isProp}(T(A))

In particular, every impredicative strictly Tarski universe is strictly impredicative.

For a universe hierarchy

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 proposition resizing 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

propresize: a:P b:P q:abisEquiv(t Ω(a,b)(q))\mathrm{propresize}:\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 impredicative.

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

See also

References

Last revised on October 15, 2022 at 12:30:10. See the history of this page for a list of all contributions to it.