nLab Coquand universe

Redirected from "Coquand universes".

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

In dependent type theory, Coquand universes or universes à la Coquand are an alternative to Russell universes and Tarski universes in presenting types and the hierarchy of type universes. Unlike type theories with Russell universes, which usually have either no separate type judgment, like that found in the HoTT book, or one type judgment, or type theories with Tarski universe, which are required to have one type judgment, type theories with Coquand universes have a type judgment for every universe in the type theory.

Formal definition

With a type judgment for each universe

One formal definition of a type theory with Coquand 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.

This allows us to add 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, as well as term judgments a:Aa:A. Then, one has the following inference rules for Coquand universes:

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

There are also weak versions of Coquand universes, where one uses identifications and equivalences of types instead of judgmental equality:

ΓilevelΓAtype iΓβ U i A:El i(Code i(A))AΓilevelΓB:U iΓη U i(B):Code i(El(B))= U iB\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{type}_i}{\Gamma \vdash \beta_{U_i}^A:\mathrm{El}_i(\mathrm{Code}_i(A)) \simeq A} \qquad \frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash B:U_i}{\Gamma \vdash \eta_{U_i}(B):\mathrm{Code}_i(\mathrm{El}(B)) =_{U_i} B}

The univalence axiom for Coquand universes states that for all A:U iA:U_i and B:U iB:U_i, transport across Lift i(El i())\mathrm{Lift}_i(\mathrm{El}_i(-)) is an equivalence of types

ΓilevelΓA:U iΓB:U iΓua U i(A,B):isEquiv(transport x:U i.Lift i(El i(x))(A,B))\frac{\Gamma \vdash i \; \mathrm{level} \quad \Gamma \vdash A:U_i \quad \Gamma \vdash B:U_i}{\Gamma \vdash \mathrm{ua}_{U_i}(A, B):\mathrm{isEquiv}(\mathrm{transport}_{x:U_i.\mathrm{Lift}_i(\mathrm{El}_i(x))}(A, B))}

With a single separate type judgment

It is also possible to define the hierarchy of Coquand universes with a single separate type judgment, such that every single type is in a Coquand 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 Coquand 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ΓCode(n)(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 \mathrm{Code}(n)(A):U(\mathrm{Level}(A))}
Γn:ΓA:U(n)ΓEl(n,A)typeΓn:ΓA:U(n)ΓLevel(El(n,A))n:\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma \vdash \mathrm{El}(n, A) \; \mathrm{type}} \quad \frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma \vdash \mathrm{Level}(\mathrm{El}(n, A)) \equiv n:\mathbb{N}}
Γn:ΓA:U(n)ΓCode(n)(El(n,A))A:U(n)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma \vdash \mathrm{Code}(n)(\mathrm{El}(n, A)) \equiv A:U(n)}
ΓAtypeΓEl(n,Code(n)(A))AtypeΓAtypeΓLevel(El(n,Code(n)(A)))Level(A):\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{El}(n, \mathrm{Code}(n)(A)) \equiv A \; \mathrm{type}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{Level}(\mathrm{El}(n, \mathrm{Code}(n)(A))) \equiv \mathrm{Level}(A):\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 El(s(n),Lift(A))\mathrm{El}(s(n), \mathrm{Lift}(A)) is a negative copy of El(n,A)\mathrm{El}(n, A):

Γ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:El(n,A)LiftEl(A)(x):El(s(n),Lift(A))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, x:\mathrm{El}(n, A) \vdash \mathrm{LiftEl}(A)(x):\mathrm{El}(s(n), \mathrm{Lift}(A))}
Γn:ΓA:U(n)Γ,y:El(s(n),Lift(A))LiftEl(A) 1(y):El(n,A)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, y:\mathrm{El}(s(n), \mathrm{Lift}(A)) \vdash \mathrm{LiftEl}(A)^{-1}(y):\mathrm{El}(n, A)}
Γn:ΓA:U(n)Γ,x:El(n,A)LiftEl(A) 1(LiftEl(A)(x))x:El(n,A)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, x:\mathrm{El}(n, A) \vdash \mathrm{LiftEl}(A)^{-1}(\mathrm{LiftEl}(A)(x)) \equiv x:\mathrm{El}(n, A)}
Γn:ΓA:U(n)Γ,y:El(s(n),Lift(A))LiftEl(A)(LiftEl(A) 1(y))y:El(s(n),Lift(A))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n)}{\Gamma, y:\mathrm{El}(s(n), \mathrm{Lift}(A)) \vdash \mathrm{LiftEl}(A)(\mathrm{LiftEl}(A)^{-1}(y)) \equiv y:\mathrm{El}(s(n), \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:El(n,A)b(x):El(n,B)Γλx:A.b(x):El(n,A nB)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma, x:\mathrm{El}(n, A) \vdash b(x):\mathrm{El}(n, B)}{\Gamma \vdash \lambda x:A.b(x):\mathrm{El}(n, A \to_{n} B)}
Γn:ΓA:U(n)ΓB:U(n)Γb:El(n,A nB)Γ,x:El(n,A)b(x):El(n,B)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma \vdash b:\mathrm{El}(n, A \to_{n} B)}{\Gamma, x:\mathrm{El}(n, A) \vdash b(x):\mathrm{El}(n, B)}
Γn:ΓA:U(n)ΓB:U(n)Γ,x:El(n,A)b(x):El(n,B)Γ,x:El(n,A)(λx:A.b(x))(x)b(x):El(n,B)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma, x:\mathrm{El}(n, A) \vdash b(x):\mathrm{El}(n, B)}{\Gamma, x:\mathrm{El}(n, A) \vdash (\lambda x:A.b(x))(x) \equiv b(x):\mathrm{El}(n, B)}
Γn:ΓA:U(n)ΓB:U(n)Γb:El(n,A nB)Γλx:A.b(x)b:El(n,A nB)\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:U(n) \quad \Gamma \vdash b:\mathrm{El}(n, A \to_{n} B)}{\Gamma \vdash \lambda x:A.b(x) \equiv b:\mathrm{El}(n, A \to_{n} B)}

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

Γn:ΓA:U(n)ΓB:El(s(n),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{El}(s(n), \mathrm{Lift}(A)) \to_{s(n)} U(n)}{\Gamma \vdash \Pi(n, A, B):U(n)}
Γn:ΓA:U(n)ΓB:El(s(n),Lift(A)) s(n)U(n)Γ,x:El(n,A)b(x):El(n,B(LiftEl(A)(x)))Γλx:A.b(x):El(n,Π(n,A,B))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{El}(s(n), \mathrm{Lift}(A)) \to_{s(n)} U(n) \quad \Gamma, x:\mathrm{El}(n, A) \vdash b(x):\mathrm{El}(n, B(\mathrm{LiftEl}(A)(x)))}{\Gamma \vdash \lambda x:A.b(x):\mathrm{El}(n, \Pi(n, A, B))}
Γn:ΓA:U(n)ΓB:El(s(n),Lift(A)) s(n)U(n)Γb:El(n,Π(n,A,B))Γ,x:El(n,A)b(x):El(n,B(LiftEl(A)(x)))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{El}(s(n), \mathrm{Lift}(A)) \to_{s(n)} U(n) \quad \Gamma \vdash b:\mathrm{El}(n, \Pi(n, A, B))}{\Gamma, x:\mathrm{El}(n, A) \vdash b(x):\mathrm{El}(n, B(\mathrm{LiftEl}(A)(x)))}
Γn:ΓA:U(n)ΓB:El(s(n),Lift(A)) s(n)U(n)Γ,x:El(n,A)b(x):El(n,B(LiftEl(A)(x)))Γ,x:El(n,A)(λx:A.b(x))(x)b(x):El(n,B(LiftEl(A)(x)))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{El}(s(n), \mathrm{Lift}(A)) \to_{s(n)} U(n) \quad \Gamma, x:\mathrm{El}(n, A) \vdash b(x):\mathrm{El}(n, B(\mathrm{LiftEl}(A)(x)))}{\Gamma, x:\mathrm{El}(n, A) \vdash (\lambda x:A.b(x))(x) \equiv b(x):\mathrm{El}(n, B(\mathrm{LiftEl}(A)(x)))}
Γn:ΓA:U(n)ΓB:El(s(n),Lift(A)) s(n)U(n)Γb:El(n,Π(n,A,B))Γλx:A.b(x)b:El(n,Π(n,A,B))\frac{\Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash A:U(n) \quad \Gamma \vdash B:\mathrm{El}(s(n), \mathrm{Lift}(A)) \to_{s(n)} U(n) \quad \Gamma \vdash b:\mathrm{El}(n, \Pi(n, A, B))}{\Gamma \vdash \lambda x:A.b(x) \equiv b:\mathrm{El}(n, \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)Code(0)()\mathrm{Nat}(0) \equiv \mathrm{Code}(0)(\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):El(n,Nat(n))\mathrm{zero}(n):\mathrm{El}(n, \mathrm{Nat}(n)) and function succ(n):El(n,Nat(n) nNat(n))\mathrm{succ}(n):\mathrm{El}(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)Code(0)():U(0)ΓctxΓ,n:Nat(s(n))Lift(Nat(n)):U(s(n))\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Nat}(0) \equiv \mathrm{Code}(0)(\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):El(n,Nat(n))ΓctxΓ,n:succ(n):El(n,Nat(n) nNat(n))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{zero}(n):\mathrm{El}(n, \mathrm{Nat}(n))} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \mathrm{succ}(n):\mathrm{El}(n, \mathrm{Nat}(n) \to_{n} \mathrm{Nat}(n))}
ΓctxΓzero(0)0:El(0,Nat(0))ΓctxΓsucc(0)s:El(0,Nat(0) 0Nat(0))\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{zero}(0) \equiv 0:\mathrm{El}(0, \mathrm{Nat}(0))} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{succ}(0) \equiv s:\mathrm{El}(0, \mathrm{Nat}(0) \to_{0} \mathrm{Nat}(0))}
ΓctxΓ,n:zero(s(n))LiftEl(Nat(n))(zero(n)):El(s(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{El}(s(n), \mathrm{Nat}(s(n)))}
ΓctxΓ,n:,m:Nat(s(n))succ(s(n))LiftEl(Nat(n))(succ(n)):El(s(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{El}(s(n), \mathrm{Nat}(s(n)) \to_{s(n)} \mathrm{Nat}(s(n)))}
  • Elimination rules for natural numbers types:
Γn:ΓC:El(s(n),Lift(Nat(n)) s(n)U(n))Γc 0:El(n,C(LiftEl(Nat(n))(zero(n)))) Γc s:El(n,Π(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):El(n,Π(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{El}(s(n), \mathrm{Lift}(\mathrm{Nat}(n)) \to_{s(n)} U(n)) \quad \Gamma \vdash c_0:\mathrm{El}(n, C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n)))) \\ \Gamma \vdash c_s:\mathrm{El}(n, \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{El}(n, \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:El(s(n),Lift(Nat(n)) s(n)U(n))Γc 0:El(n,C(LiftEl(Nat(n))(zero(n)))) Γc s:El(n,Π(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:El(n,C(LiftEl(Nat(n))(zero(n))))\frac{ \begin{array}{c} \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash C:\mathrm{El}(s(n), \mathrm{Lift}(\mathrm{Nat}(n)) \to_{s(n)} U(n)) \quad \Gamma \vdash c_0:\mathrm{El}(n, C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n)))) \\ \Gamma \vdash c_s:\mathrm{El}(n, \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:\mathrm{El}(n, C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n))))}
Γn:ΓC:El(s(n),Lift(Nat(n)) s(n)U(n))Γc 0:El(n,C(LiftEl(Nat(n))(zero(n)))) Γc s:El(n,Π(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)):El(n,C(LiftEl(Nat(n))(succ(n,x))))\frac{ \begin{array}{c} \Gamma \vdash n:\mathbb{N} \quad \Gamma \vdash C:\mathrm{El}(s(n), \mathrm{Lift}(\mathrm{Nat}(n)) \to_{s(n)} U(n)) \quad \Gamma \vdash c_0:\mathrm{El}(n, C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{zero}(n)))) \\ \Gamma \vdash c_s:\mathrm{El}(n, \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)):\mathrm{El}(n, C(\mathrm{LiftEl}(\mathrm{Nat}(n))(\mathrm{succ}(n, x))))}

Something similar could be done for Russell universes.

Analogues in set theory

There are analogues of Coquand universes 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 Coquand 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 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 Coquand universes:

ΓκlevelΓV κset κ +ΓκlevelΓAset κΓCode κ(A)set κ +\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 \mathrm{Code}_{\kappa}(A) \; \mathrm{set}_{\kappa^+}}
ΓκlevelΓAset κΓCode κ(A) κ +V κtrueΓκlevelΓAset κ +ΓA κ +V κtrueΓEl κ(A)set κ\frac{\Gamma \vdash \kappa \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{set}_\kappa}{\Gamma \vdash \mathrm{Code}_{\kappa}(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 \mathrm{El}_{\kappa}(A) \; \mathrm{set}_\kappa}
ΓκlevelΓAset κΓEl κ(Code κ(A))=AtrueΓκlevelΓAset κ +ΓA κ +V κtrueΓCode κ(El κ(A))=Atrue\frac{\Gamma \vdash \kappa \; \mathrm{level} \quad \Gamma \vdash A \; \mathrm{set}_\kappa}{\Gamma \vdash \mathrm{El}_{\kappa}(\mathrm{Code}_{\kappa}(A)) = A \; \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 \mathrm{Code}_{\kappa}(\mathrm{El}_{\kappa}(A)) = A \; \mathrm{true}}

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

 References

Universes à la Coquand are described in section 2.1 of

Last revised on January 16, 2024 at 02:06:27. See the history of this page for a list of all contributions to it.