Russell universe (changes) in nLab
Showing changes from revision #15 to #16: Added | Removed | Changed
Context
Type theory
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = \linebreak propositions as types +programs as proofs +relation type theory/category theory
Universes
\tableofcontents
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.
Formal Definition 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 i≡U 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
If It is also possible to define the type hierarchy theory of has Russell universes with a single separate type judgment 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:AtypeA \; \mathrm{type}, the rules for Russell universes become simpler, as one doesn’t have to assume infinitely many Russell universes and a second level to house the natural numbers type used to index the universes. Instead, we merely have
ΓctxΓ⊢ U ℕtypeΓ⊢A:UΓ⊢AtypeΓ⊢Level(A):ℕ \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash U \mathbb{N} \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:U}{\Gamma \vdash A \; \mathrm{type}} \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))}
Furthermore, the separate type judgment amounts to collapsing the two levels in the theory above into one level: Instead of defining the identity type and the type of natural numbers as external to the type theory, we instead define it as normal types internal to the type theory. Then the rules for the infinite tower of Russell universes are as follows:
Γ⊢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}}
Γ⊢ i ctx:ℕΓ ⊢ , U n(i): U ℕ ( ⊢s( i n) ) :ℕΓ⊢ i ctx:ℕΓ⊢A:U(i)Γ,n:ℕ⊢ A Level( type U(n))≡s(n):ℕΓ⊢i:ℕΓ⊢A:U(i)Γ⊢Lift(i)(A):U(s(i)) \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash i:\mathbb{N}}{\Gamma s(n):\mathbb{N}} \vdash U(i):U(s(i))} \qquad \frac{\Gamma \vdash i:\mathbb{N} \quad \Gamma \vdash A:U(i)}{\Gamma \vdash A \; \mathrm{type}} \mathrm{ctx}}{\Gamma, \qquad n:\mathbb{N} \frac{\Gamma \vdash i:\mathbb{N} \mathrm{Level}(U(n)) \quad \equiv \Gamma s(n):\mathbb{N}} \vdash A:U(i)}{\Gamma \vdash \mathrm{Lift}(i)(A):U(s(i))}
We In could particular, also add rules which state that every type is an element of a Russell universe: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).
Γ⊢AtypeΓ⊢level A:ℕΓ⊢AtypeΓ⊢A:U(level A)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{level}_A:\mathbb{N}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A:U(\mathrm{level}_A)} 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: Then the first rule for the infinite tower becomes one of Γ⊢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:A⊢LiftEl(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)} Γ⊢ i n:ℕΓ⊢A:U(n)Γ,y:Lift(A)⊢level U(i)LiftEl≡s( i A) −1(y): ℕ AstrictΓ⊢i:ℕΓ⊢defLevelU(i):level U(i)= ℕs(i)weak \frac{\Gamma \vdash i:\mathbb{N}}{\Gamma n:\mathbb{N} \vdash \mathrm{level}_{U(i)} \equiv s(i):\mathbb{N}}\mathrm{strict} \quad \frac{\Gamma \Gamma \vdash i:\mathbb{N}}{\Gamma A:U(n)}{\Gamma, y:\mathrm{Lift}(A) \vdash \mathrm{defLevelU}(i):\mathrm{level}_{U(i)} \mathrm{LiftEl}(A)^{-1}(y):A} =_\mathbb{N} s(i)}\mathrm{weak} Γ⊢n:ℕΓ⊢A:U(n)Γ,x:A⊢LiftEl(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} This is how one would formally present a dependent type theory like the one in Book HoTT or the ones in Agda, Coq, Lean, without resorting to external layers. Γ⊢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)} However, Next these set of rules are incompatible with the statement rules that for all dependent function sum types , exist, which because are the necessary dependent to sum define type∑ n:ℕU(n)\sum_{n:\mathbb{N}} U(n)type families contains as elements pairs of every a type in for the type theory and the universe level the type is in. However, by the inference rules above,∑ n:ℕU(n)\sum_{n:\mathbb{N}} U(n)dependent product types is and in the universe induction principle of theU(level ∑ n:ℕU(n))U(\mathrm{level}_{\sum_{n:\mathbb{N}} U(n)})natural numbers type . which Here, means that by right projecting∑ n:ℕU(n)\sum_{n:\mathbb{N}} U(n)function types , every are type indexed is by in the universe level U n(level ∑ n:ℕU(n)) U(\mathrm{level}_{\sum_{n:\mathbb{N}} n U(n)}) , resulting since in the function type indexed byGirard's paradoxnn which are is only contradictory. definable forU(n)U(n)-small types, aka types with level nn. Instead, usually the inference rules for dependent sum types require that the type family x:A⊢B(x)x:A \vdash B(x) in the dependent sum type have the same universe level n:ℕn:\mathbb{N}, x:A⊢B(x):U(n)x:A \vdash B(x):U(n). Since none of the universes in the above diagram have the same universe level, the dependent sum type ∑ n:ℕU(n)\sum_{n:\mathbb{N}} U(n) cannot be constructed. The same is true of the formers of any type which could construct dependent sum types, such as wide pushouts. Γ⊢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:A⊢b(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} Similarly, these set of rules are incompatible with the statement that all sequential colimits exist, because one could then find the sequential colimit of the diagram Γ⊢n:ℕΓ⊢A:U(n)Γ⊢B:U(n)Γ⊢b:A→ nBΓ,x:A⊢b(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:A⊢b(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} UΓ⊢n:ℕΓ⊢A:U(n)Γ⊢B:U(n)Γ⊢b:A→ nBΓ⊢λx:A.b(x)≡b:A→ nB(0)→Lift(0)U(s(0))→Lift(s(0))U(s(s(0)))→Lift(s(s(0)))… U(0) \frac{\Gamma \overset{\mathrm{Lift}(0)}\to \vdash U(s(0)) n:\mathbb{N} \overset{\mathrm{Lift}(s(0))}\to \quad U(s(s(0))) \Gamma \overset{\mathrm{Lift}(s(s(0)))}\to \vdash \ldots 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} and Similarly, one the would rules get for a dependent type function types are as follows:U ∞U_\infty, which by definition of sequential colimits contains every type in the universe hierarchy. However, U ∞U_\infty is in the universe U(level U ∞)U(\mathrm{level}_{U_\infty}), which means that lifting U ∞U_\infty from U(level U ∞)U(\mathrm{level}_{U_\infty}) to U ∞U_\infty via the sequential colimit results in Girard's paradox which is contradictory. Instead, usually the inference rules for sequential colimits require that the types in the above diagram have the same universe level n:ℕn:\mathbb{N}. Since none of the universes in the above diagram have the same universe level, the sequential colimit U ∞U_\infty cannot be constructed. The same is true of the formers of any type which could construct sequential colimits, such as pushout types. Γ⊢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:A⊢b(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)} But none of this are problems in Book HoTT as the formers for every type have the same universe level as the type to be put in the universe. Γ⊢n:ℕΓ⊢A:U(n)Γ⊢B:Lift(A)→ s(n)U(n)Γ⊢b:Π(n,A,B)Γ,x:A⊢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 \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:A⊢b(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). Γ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))} Γ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))} Γ⊢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)}
Γ⊢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. There are analogues of cumulative Russell universes in set theory. 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 a∈Aa \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Γ⊢A∈V κtrueΓ⊢A∈V κ +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} 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. The notion is due to: For more see the references at type universe.
Analogues in set theory
With a single set judgment
With a separate set judgment for each set theory
See also
References
Last revised on January 16, 2024 at 01:24:44. See the history of this page for a list of all contributions to it.