nLab Russell universe

Redirected from "à la Russell".

Context

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

Universes

Contents

Idea

Russell universes or universes à la Russell are types whose terms are types. In type theories without a separate type judgment AtypeA \; \mathrm{type}, only typing judgments a:Aa:A, what would have been type judgments are represented by typing judgments that AA is a term of a Russell universe UU, A:UA:U. Russell universes without a separate type judgment are used in many places in type theory, including in the HoTT book, in Coq, and in Agda.

Definition of a single Russell universe

If the type theory has a separate type judgment AtypeA \; \mathrm{type}, then one could define a single Russell universe in the type theory. We merely have

ΓctxΓUtypeΓA:UΓAtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash U \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:U}{\Gamma \vdash A \; \mathrm{type}}

Formal definition of a hierarchy of Russell universes

Dependent type theories typically come with a hierarchy of Russell universes, so that all types in the dependent type theory are elements of Russell universes. This is especially the case for dependent type theories without any separate type judgments at all, where types are necessarily defined as terms of Russell universes.

Without a separate type judgment

One formal definition of a type theory with a hierarchy of Russell universes is as follows:

The type theory has judgments

  • Γctx\Gamma \; \mathrm{ctx}, that Γ\Gamma is a context

  • ileveli \; \mathrm{level}, that ii is a universe level,

  • ϕprop\phi \; \mathrm{prop}, that ϕ\phi is a proposition,

  • ϕtrue\phi \; \mathrm{true}, that ϕ\phi is a true proposition,

and consists of the formal signature and inference rules of first-order Heyting arithmetic or Peano arithmetic. These rules ensure that there are an infinite number of indices, which are strictly ordered with strict total order <\lt and upwardly unbounded, where i<s(i)i \lt s(i) is true for all indices ii.

Now, we introduce the typing judgment a:Aa:A, which says that aa is a term of the type AA. Instead of type judgments, we introduce a special kind of type called a Russell universe or universe à la Russell, whose terms are the types themselves. Russell universes are formalized with the following rules:

ΓilevelΓU i:U s(i)ΓilevelΓA:U iΓA:U s(i)cumulΓilevelΓA:U iΓLift i,j(A):U s(i)lifting\frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash U_i:U_{s(i)}} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{\Gamma \vdash A:U_{s(i)}}\mathrm{cumul} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{\Gamma \vdash \mathrm{Lift}_{i, j}(A):U_{s(i)}}\mathrm{lifting}

In addition, we have rules for contexts which state that one could add typing judgments to the list of contexts:

ΓilevelΓA:U i(Γ,a:A)ctx\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{(\Gamma, a:A) \; \mathrm{ctx}}

as well as rules saying that equality is preserved across universe levels:

ΓilevelΓjlevelΓi=jtrueΓU iU j:U s(i)judgmentalΓilevelΓjlevelΓi=jtrueΓap U i=j:U i= U s(i)U jtypal\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash j \; \mathrm{level} \quad \Gamma \vdash i = j \; \mathrm{true}}{\Gamma \vdash U_i \equiv U_j:U_{s(i)}}\mathrm{judgmental} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash j \; \mathrm{level} \quad \Gamma \vdash i = j \; \mathrm{true}}{\Gamma \vdash \mathrm{ap}_U^{i = j}:U_i =_{U_{s(i)}} U_j}\mathrm{typal}

With a type judgment for each universe

One could also define a hierarchy of Russell universes à la Coquand, in that the type theory has a type judgment for each universe UU. Using the dependent type theory with no separate type judgment, instead of having only one term judgment a:Aa:A, for level ii and type A:U iA:U_i, we instead have an infinite number of type judgments, one type judgment Atype iA \; \mathrm{type}_i for every level ii, indicating that AA is a type with level ii, in addition to the term judgments a:Aa:A. Then, one has the following rules for Russell universes à la Coquand:

ΓilevelΓU itype s(i)ΓilevelΓAtype iΓAtype s(i)cumulΓilevelΓAtype iΓLift(A)type s(i)lifting\frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash U_i \; \mathrm{type}_{s(i)}} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i}{\Gamma \vdash A \; \mathrm{type}_{s(i)}}\mathrm{cumul} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i}{\Gamma \vdash \mathrm{Lift}(A) \; \mathrm{type}_{s(i)}}\mathrm{lifting}
ΓilevelΓAtype iΓA:U iΓilevelΓA:U iΓAtype i\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i}{\Gamma \vdash A:U_i} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{\Gamma \vdash A \; \mathrm{type}_i}

In addition, we have rules for contexts which state that one could add typing judgments to the list of contexts:

ΓilevelΓAtype i(Γ,a:A)ctx\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i}{(\Gamma, a:A) \; \mathrm{ctx}}

One could derive from these rules the above rules for Russell universes and context extension

ΓilevelΓU i:U s(i)ΓilevelΓA:U iΓA:U s(i)cumulΓilevelΓA:U iΓLift(A):U s(i)lifting\frac{\Gamma \vdash i \; \mathrm{level}}{\Gamma \vdash U_i:U_{s(i)}} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{\Gamma \vdash A:U_{s(i)}}\mathrm{cumul} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{\Gamma \vdash \mathrm{Lift}(A):U_{s(i)}}\mathrm{lifting}
ΓilevelΓA:U i(Γ,a:A)ctx\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i}{(\Gamma, a:A) \; \mathrm{ctx}}

With a single separate type judgment

It is also possible to define the hierarchy of Russell universes with a single separate type judgment, such that every single type is in a Russell universe. The advantage of doing so is that one doesn’t need to define the theory of universe levels before defining the type theory; one could instead simply define the natural numbers inside of the type theory itself, along with the hierarchy of Russell universes:

ΓctxΓtypeΓAtypeΓLevel(A):\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{Level}(A):\mathbb{N}}
ΓctxΓ,n:U(n)typeΓAtypeΓA:U(Level(A))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash U(n) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A:U(\mathrm{Level}(A))}
Γn:ΓA:U(n)ΓAtypeΓn:ΓA:U(n)ΓLevel(A)n:\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma \vdash A \; \mathrm{type}} \quad \frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma \vdash \mathrm{Level}(A) \equiv n:\mathbb{N}}
ΓctxΓ0:ΓctxΓLevel()0:\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Level}(\mathbb{N}) \equiv 0:\mathbb{N}}
ΓctxΓ,n:s(n):ΓctxΓ,n:Level(U(n))s(n):\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash s(n):\mathbb{N}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{Level}(U(n)) \equiv s(n):\mathbb{N}}

In particular, every type AA has a universe level, which is a natural number, and the universe level of \mathbb{N} is zero and the universe level of U(n)U(n) given natural number nn is the successor s(n)s(n).

Furthermore, every type AA of level nn lifts to another type Lift(A)\mathrm{Lift}(A) of level s(n)s(n), such that Lift(A)\mathrm{Lift}(A) is a negative copy of AA:

Γn:ΓA:U(n)ΓLift(A):U(s(n))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma \vdash \mathrm{Lift}(A):U(s(n))}
Γn:ΓA:U(n)Γ,x:ALiftEl(A)(x):Lift(A)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, x:A \vdash \mathrm{LiftEl}(A)(x):\mathrm{Lift}(A)}
Γn:ΓA:U(n)Γ,y:Lift(A)LiftEl(A) 1(y):A\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, y:\mathrm{Lift}(A) \vdash \mathrm{LiftEl}(A)^{-1}(y):A}
Γn:ΓA:U(n)Γ,x:ALiftEl(A) 1(LiftEl(A)(x))x:A\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, x:A \vdash \mathrm{LiftEl}(A)^{-1}(\mathrm{LiftEl}(A)(x)) \equiv x:A}
Γn:ΓA:U(n)Γ,y:Lift(A)LiftEl(A)(LiftEl(A) 1(y))y:Lift(A)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, y:\mathrm{Lift}(A) \vdash \mathrm{LiftEl}(A)(\mathrm{LiftEl}(A)^{-1}(y)) \equiv y:\mathrm{Lift}(A)}

Next are the rules for function types, which are necessary to define type families as elements of a type for dependent product types and the induction principle of the natural numbers type. Here, function types are indexed by the universe level nn, since the function type indexed by nn are only definable for U(n)U(n)-small types, aka types with level nn.

Γn:ΓA:U(n)ΓB:U(n)ΓA nB:U(n)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n)}{\Gamma \vdash A \to_{n} B:U(n)}
Γn:ΓA:U(n)ΓB:U(n)Γ,x:Ab(x):BΓλx:A.b(x):A nB\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma, x:A \vdash b(x):B}{\Gamma \vdash \lambda x:A.b(x):A \to_{n} B}
Γn:ΓA:U(n)ΓB:U(n)Γb:A nBΓ,x:Ab(x):B\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma \vdash b:A \to_{n} B}{\Gamma, x:A \vdash b(x):B}
Γn:ΓA:U(n)ΓB:U(n)Γ,x:Ab(x):BΓ,x:A(λx:A.b(x))(x)b(x):B\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma, x:A \vdash b(x):B}{\Gamma, x:A \vdash (\lambda x:A.b(x))(x) \equiv b(x):B}
Γn:ΓA:U(n)ΓB:U(n)Γb:A nBΓλx:A.b(x)b:A nB\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma \vdash b:A \to_{n} B}{\Gamma \vdash \lambda x:A.b(x) \equiv b:A \to_{n} B}

Similarly, the rules for dependent function types are as follows:

Γn:ΓA:U(n)ΓB:Lift(A) s(n)U(n)ΓΠ(n,A,B):U(n)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{Lift}(A) \to_{s(n)} U(n)}{\Gamma \vdash \Pi(n, A, B):U(n)}
Γn:ΓA:U(n)ΓB:Lift(A) s(n)U(n)Γ,x:Ab(x):B(LiftEl(A)(x))Γλx:A.b(x):Π(n,A,B)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{Lift}(A) \to_{s(n)} U(n) \quad \Gamma, x:A \vdash b(x):B(\mathrm{LiftEl}(A)(x))}{\Gamma \vdash \lambda x:A.b(x):\Pi(n, A, B)}
Γn:ΓA:U(n)ΓB:Lift(A) s(n)U(n)Γb:Π(n,A,B)Γ,x:Ab(x):B(LiftEl(A)(x))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{Lift}(A) \to_{s(n)} U(n) \quad \Gamma \vdash b:\Pi(n, A, B)}{\Gamma, x:A \vdash b(x):B(\mathrm{LiftEl}(A)(x))}
Γn:ΓA:U(n)ΓB:Lift(A) s(n)U(n)Γ,x:Ab(x):B(LiftEl(A)(x))Γ,x:A(λx:A.b(x))(x)b(x):B(LiftEl(A)(x))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{Lift}(A) \to_{s(n)} U(n) \quad \Gamma, x:A \vdash b(x):B(\mathrm{LiftEl}(A)(x))}{\Gamma, x:A \vdash (\lambda x:A.b(x))(x) \equiv b(x):B(\mathrm{LiftEl}(A)(x))}
Γn:ΓA:U(n)ΓB:Lift(A) s(n)U(n)Γb:Π(n,A,B)Γλx:A.b(x)b:Π(n,A,B)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{Lift}(A) \to_{s(n)} U(n) \quad \Gamma \vdash b:\Pi(n, A, B)}{\Gamma \vdash \lambda x:A.b(x) \equiv b:\Pi(n, A, B)}

Finally, we have for each universe level n:n:\mathbb{N} a natural numbers type Nat(n)\mathrm{Nat}(n) such that Nat(0)\mathrm{Nat}(0) \equiv \mathbb{N} and Nat(s(n))Lift(Nat(n))\mathrm{Nat}(s(n)) \equiv \mathrm{Lift}(\mathrm{Nat}(n)). In addition, each Nat(n)\mathrm{Nat}(n) has element zero(n):Nat(n)\mathrm{zero}(n):\mathrm{Nat}(n) and function succ(n):Nat(n) nNat(n)\mathrm{succ}(n):\mathrm{Nat}(n) \to_{n} \mathrm{Nat}(n), defined via lifting the elements of Nat(n)\mathrm{Nat}(n) across universe levels. Finally, each Nat(n)\mathrm{Nat}(n) satisfies the induction principle of the natural numbers type over the universe U(n)U(n).

  • Formation rules for natural numbers types:
ΓctxΓ,n:Nat(n):U(n)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{Nat}(n):U(n)}
ΓctxΓNat(0):U(0)ΓctxΓ,n:Nat(s(n))Lift(Nat(n)):U(s(n))\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Nat}(0) \equiv \mathbb{N}:U(0)} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{Nat}(s(n)) \equiv \mathrm{Lift}(\mathrm{Nat}(n)):U(s(n))}
  • Introduction rules for natural numbers types:
ΓctxΓ,n:zero(n):Nat(n)ΓctxΓ,n:succ(n):Nat(n) nNat(n)\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{zero}(n):\mathrm{Nat}(n)} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{succ}(n):\mathrm{Nat}(n) \to_{n} \mathrm{Nat}(n)}
ΓctxΓzero(0)0:Nat(0)ΓctxΓsucc(0)s:Nat(0) 0Nat(0)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{zero}(0) \equiv 0:\mathrm{Nat}(0)} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{succ}(0) \equiv s:\mathrm{Nat}(0) \to_{0} \mathrm{Nat}(0)}
ΓctxΓ,n:zero(s(n))LiftEl(Nat(n))(zero(n)):Nat(s(n))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{zero}(s(n)) \equiv \mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n)):\mathrm{Nat}(s(n))}
ΓctxΓ,n:,m:Nat(s(n))succ(s(n))LiftEl(Nat(n))(succ(n)):Nat(s(n)) s(n)Nat(s(n))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N}, m:\mathrm{Nat}(s(n)) \vdash \mathrm{succ}(s(n)) \equiv \mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{succ}(n)):\mathrm{Nat}(s(n)) \to_{s(n)} \mathrm{Nat}(s(n))}
  • Elimination rules for natural numbers types:
Γn:ΓC:Lift(Nat(n)) s(n)U(n)Γc 0:C(LiftEl(Nat(n))(zero(n))) Γc s:Π(n,Nat(n),λx:Nat(n).C(LiftEl(Nat(n))(x)) nC(LiftEl(Nat(n))(succ(n,x)))) Γind Nat(n,C,c 0,c s):Π(n,Nat(n),λx:Nat(n).C(LiftEl(Nat(n))(x)))\frac{ \begin{array}{c} \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash C:\mathrm{Lift}(\mathrm{Nat}(n)) \to_{s(n)} U(n) \quad \Gamma \vdash c_0:C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n))) \\ \Gamma \vdash c_s:\Pi\left(n, \mathrm{Nat}(n), \lambda x:\mathrm{Nat}(n).C(\mathrm{LiftEl}(\mathrm{Nat}(n))(x)) \to_{n} C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{succ}(n, x)))\right) \\ \end{array}}{\Gamma \vdash \mathrm{ind}_\mathrm{Nat}(n, C, c_0, c_s):\Pi\left(n, \mathrm{Nat}(n), \lambda x:\mathrm{Nat}(n).C(\mathrm{LiftEl}(\mathrm{Nat}(n))(x))\right)}
  • Computation rules for natural numbers types:
Γn:ΓC:Lift(Nat(n)) s(n)U(n)Γc 0:C(LiftEl(Nat(n))(zero(n))) Γc s:Π(n,Nat(n),λx:Nat(n).C(LiftEl(Nat(n))(x)) nC(LiftEl(Nat(n))(succ(n,x)))) Γind Nat(n,C,c 0,c s,zero(n))c 0:C(LiftEl(Nat(n))(zero(n)))\frac{ \begin{array}{c} \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash C:\mathrm{Lift}(\mathrm{Nat}(n)) \to_{s(n)} U(n) \quad \Gamma \vdash c_0:C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n))) \\ \Gamma \vdash c_s:\Pi\left(n, \mathrm{Nat}(n), \lambda x:\mathrm{Nat}(n).C(\mathrm{LiftEl}(\mathrm{Nat}(n))(x)) \to_{n} C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{succ}(n, x)))\right) \\ \end{array}}{\Gamma \vdash \mathrm{ind}_\mathrm{Nat}(n, C, c_0, c_s, \mathrm{zero}(n)) \equiv c_0:C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n)))}
Γn:ΓC:Lift(Nat(n)) s(n)U(n)Γc 0:C(LiftEl(Nat(n))(zero(n))) Γc s:Π(n,Nat(n),λx:Nat(n).C(LiftEl(Nat(n))(x)) nC(LiftEl(Nat(n))(succ(n,x)))) Γ,x:Nat(n)ind Nat(n,C,c 0,c s,succ(n,x))c s(ind Nat(n,C,c 0,c s,x)):C(LiftEl(Nat(n))(succ(n,x)))\frac{ \begin{array}{c} \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash C:\mathrm{Lift}(\mathrm{Nat}(n)) \to_{s(n)} U(n) \quad \Gamma \vdash c_0:C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n))) \\ \Gamma \vdash c_s:\Pi\left(n, \mathrm{Nat}(n), \lambda x:\mathrm{Nat}(n).C(\mathrm{LiftEl}(\mathrm{Nat}(n))(x)) \to_{n} C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{succ}(n, x)))\right) \\ \end{array}}{\Gamma, x:\mathrm{Nat}(n) \vdash \mathrm{ind}_\mathrm{Nat}(n, C, c_0, c_s, \mathrm{succ}(n, x)) \equiv c_s(\mathrm{ind}_\mathrm{Nat}(n, C, c_0, c_s, x)):C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{succ}(n, x)))}

Something similar could be done for Coquand universes.

Analogues in set theory

There are analogues of cumulative Russell universes in set theory.

With a single set judgment

One formal definition of a set theory with cumulative Russell universes is as follows:

The set theory has judgments

  • Γctx\Gamma \; \mathrm{ctx}, that Γ\Gamma is a context

  • κlevel\kappa \; \mathrm{level}, that κ\kappa is a universe level,

  • ϕprop\phi \; \mathrm{prop}, that ϕ\phi is a proposition,

  • ϕtrue\phi \; \mathrm{true}, that ϕ\phi is a true proposition,

and consists of the formal signature and inference rules of first-order Heyting arithmetic or Peano arithmetic. These rules ensure that there are an infinite number of indices, which are strictly ordered with strict total order <\lt and upwardly unbounded, where κ<κ +\kappa \lt \kappa^+ is true for all indices κ\kappa.

Now, we introduce a single set judgment AsetA \; \mathrm{set} which says that AA is a set, as well as the membership relation aAa \in A, which says that aa in the set AA. We introduce a special kind of set called a cumulative Russell universe or cumulative universe à la Russell, which formalized with the following rules:

ΓκlevelΓV κsetΓκlevelΓV κV κ +trueΓκlevelΓAsetΓAV κtrueΓAV κ +truecumul\frac{\Gamma \vdash \kappa \; \mathrm{level}}{\Gamma \vdash V_\kappa \; \mathrm{set}} \qquad \frac{\Gamma \vdash \kappa \; \mathrm{level}}{\Gamma \vdash V_\kappa \in V_{\kappa^+} \; \mathrm{true}} \qquad \frac{\Gamma \vdash \kappa \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{set} \quad \Gamma \vdash A \in V_\kappa \; \mathrm{true}}{\Gamma \vdash A \in V_{\kappa^+} \; \mathrm{true}}\mathrm{cumul}

With a separate set judgment for each set theory

There are also analogues of cumulative Russell universes à la Coquand in set theory. Instead of having a single set theory, one has a whole collection of set theories which embed into each other, with indices indicating which level the set theory lies on.

One formal definition of a set theory with cumulative Russell universes à la Coquand is as follows:

The set theory has judgments

  • Γctx\Gamma \; \mathrm{ctx}, that Γ\Gamma is a context

  • κlevel\kappa \; \mathrm{level}, that κ\kappa is a level of set theory,

  • ϕprop\phi \; \mathrm{prop}, that ϕ\phi is a proposition,

  • ϕtrue\phi \; \mathrm{true}, that ϕ\phi is a true proposition,

and consists of the formal signature and inference rules of first-order Heyting arithmetic or Peano arithmetic. These rules ensure that there are an infinite number of indices, which are strictly ordered with strict total order <\lt and upwardly unbounded, where κ<κ +\kappa \lt \kappa^+ is true for all indices κ\kappa.

This allows us to add an infinite number of set judgments, one set judgment Aset κA \; \mathrm{set}_\kappa for every level κ\kappa, indicating that AA is a set with level κ\kappa, as well as an infinite number of membership relations x κAx \in_\kappa A, one for each set judgment set κ\mathrm{set}_\kappa. Then, one has the following inference rules for cumulative Russell universes à la Coquand:

ΓκlevelΓV κset κ +ΓκlevelΓAset κΓAset κ +\frac{\Gamma \vdash \kappa \; \mathrm{level}}{\Gamma \vdash V_\kappa \; \mathrm{set}_{\kappa^+}} \quad \frac{\Gamma \vdash \kappa \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{set}_\kappa}{\Gamma \vdash A \; \mathrm{set}_{\kappa^+}}
ΓκlevelΓAset κΓA κ +V κtrueΓκlevelΓAset κ +ΓA κ +V κtrueΓAset κ\frac{\Gamma \vdash \kappa \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{set}_\kappa}{\Gamma \vdash A \in_{\kappa^+} V_\kappa \; \mathrm{true}} \qquad \frac{\Gamma \vdash \kappa \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{set}_{\kappa^+} \quad \Gamma \vdash A \in_{\kappa^+} V_\kappa \; \mathrm{true}}{\Gamma \vdash A \; \mathrm{set}_\kappa}

This says that each V κV_\kappa is a set which satisfies a reflection principle.

See also

References

The notion is due to:

For more see the references at type universe.

Last revised on January 16, 2024 at 01:24:44. See the history of this page for a list of all contributions to it.