ncatlab.org

type universe in nLab

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

homotopy levels

semantics

Contents

Idea

In type theory, a type universe – usually written 𝒰\mathcal{U} or TypeType – is a type whose terms are either themselves types (Russell universes), or representations of types in an internal model of the type theory (Tarski universes). Either way, it is a universe of (small) types, a universe in type theory, and sometimes called a type of types.

One also speaks of 𝒰\mathcal{U} as being a reflection of the type system in itself (e.g. MartinLöf 74, p. 6, Palmgren, pp. 2-3, Rathjen, p. 1, Luo 11, section 2.5, Luo 12, p. 2, Stanf. Enc. Phil.), following the reflection principle in set theory.

In homotopy type theory a type of (small) types is what in higher categorical semantics is interpreted as a (small) object classifier. Thus, the type of types is a refinement of the type of propositions which only contains the (-1)-truncated/h-level-1 types (and is semantically a subobject classifier).

In the presence of a type universe a judgement of the form

⊢A:𝒰 \vdash A : \mathcal{U}

says that AA is a term of type 𝒰\mathcal{U}, hence is either a (small) type itself (for Russell universes), or a representation of types in an internal model of the type theory (for Tarski universes).

More generally, in Russell universes a hypothetical judgement of the form

x:X⊢A(x):𝒰 x : X \vdash A(x) : \mathcal{U}

says that AA is an XX-dependent type.

In Tarski universes the corresponding hypothetical judgment would be of the form

x:X⊢El(A)(x)type x : X \vdash El(A)(x)\; type

Type universes are important in dependent type theory for numerous reasons:

  1. Dependent type theory with a separate type judgment serves as a background for a variety of foundations of mathematics via the propositions as some types interpretation of dependent type theory: One can add a von Neumann universe to the dependent type theory and work entirely in the von Neumann universe for material set theory; one can add a category of sets to the dependent type theory and work entirely in the category of sets for structural set theory; and one can add a type of all propositions and a natural numbers type and work in the dependent type theory itself for higher-order logic. For univalent type theory and univalent foundations, on the other hand, one needs to add a type universe satisfying certain axioms and axiom schemata, such as universe extensionality, closure under identity types, closure under dependent sum types, closure under dependent product types, propositional resizing, replacement, infinity, and choice, to the dependent type theory.

  2. In set theory, one could usually quantify over sets using the universal quantifier and the existential quantifier. However, in dependent type theory, one could only quantify over elements of types. Without type universes, types are not elements of type universes, but rather judged separately as a type, and thus it is impossible to quantify over types. Quantification over types is necessary for proving universal properties of various mathematical structures, such as that the integers are the initial commutative ring.

  3. Having a hierarchy of universes where every type is an element of the hierarchy, instead of a single separate type judgment has its own benefits. These includes the lack of annotations in defining types, since all types are elements of universes A:U iA:U_i and all family of types are elements of function types B:A→U iB:A \to U_i; the lack of additional rules for judgmental equality in type theories with judgmental equality, since they are all admissible; the ease of definitions of types in objective type theory which does not have judgmental equality; and the lack of separate type judgments for modes in split context modal type theory. However, this comes at the cost of having to formalize the theory of universe levels of the hierarchy of universes before formalizing the type theory.

In homotopy type theory the type universe 𝒰\mathcal{U} is often assumed to satisfy the univalence axiom. This is a reflection of the fact that in its categorical semantics as an object classifier is part of an internal (∞,1)-category in the ambient (∞,1)-topos: the one that as an indexed category is the small codomain fibration.

Per Martin-Lof‘s original type theory contained a Russell universe which contained all types, which therefore in particular contained itself, i.e. one had Type:TypeType : Type. But it was pointed out by Jean-Yves Girard that this was inconsistent; see Girard's paradox. Thus, modern type theories generally contain a hierarchy of universes.

Formalizations

Russell universe

A Russell universe or universe à la Russell is a type whose terms are types. In the presence of a separate judgment “AtypeA \;type”, this can be formulated as a deduction rule of the form

A:𝒰Atype\frac{A:\mathcal{U}}{A \;type}

Thus, the type formers have rules saying which universe they belong to, such as:

A:𝒰B:A→𝒰ΠAB:𝒰\frac{A:\mathcal{U}\quad B:A\to \mathcal{U}}{\Pi\, A\, B : \mathcal{U}}

With Russell universes, we can also omit the judgment “AtypeA\; type” and replace it everywhere by a judgment that A is a term of some universe. This is the approach taken in UFP13.

Tarski universes

A Tarski universe or a universe à la Tarski (Hofmann, section 2.1.6, Luo 12, Gallozzi 14, p. 40) is a type UU together with an “interpretation” operation allowing us to regard its terms as codes or names for actual types. Thus we have a rule such as

A:𝒰El(A)type\frac{A:\mathcal{U}}{El(A)\;type}

saying that for each term AA of the type universe UU there is an actual type El(A)El(A). This is the approach taken by Egbert Rijke‘s Introduction to Homotopy Type Theory.

Conversely, with notation as used at object classifier in an (infinity,1)-topos, one might write A=′El(A)′A = 'El(A)' to indicate that AA is the name of the type El(A)El(A) in the type universe.

We usually also have operations on the universe corresponding to (but not identical to) type formers, such as

A:𝒰B:A→𝒰π(A,B):𝒰\frac{A:\mathcal{U}\quad B:A\to \mathcal{U}}{\pi(A, B) : \mathcal{U}}

with an equality El(π(A,B))=ΠEl(A)El(B)El(\pi(A,B))=\Pi \, El(A)\, El(B). Usually this latter equality (and those for other type formers) is a judgmental equality. If it is only an equivalence (i.e. we have a rule which gives us a canonical term of the equivalence type), we may speak of a weakly Tarski universe (Gallozzi 14, p. 49-50).

We can give a slightly different definition of weakly Tarski universe using propositional equality and a larger universe. More precisely, we can consider two (or many) universes 𝒰\mathcal{U} and 𝒰′\mathcal{U}' with the usual rules for the relative reflection el(a):𝒰′el(a):\mathcal{U}' for any a:Ua:U, a choice of weakly or strongly Tarski computation rules for the reflections ElEl and El′El', and a computation rule for the relative reflection el of 𝒰\mathcal{U} inside 𝒰′\mathcal{U}' based on propositional equality, which gives us canonical elements of the identity types Id 𝒰′(π′(el(a),el(b)),el(π(a,b)))Id_{\mathcal{U}'}(\pi'(el(a),el(b)),el(\pi(a,b))) and similarly for the other type formers.

If the containing universe is univalent the two definitions turn out to coincide.

The three notions of Tarski universe can be ordered by generality: Every Tarski universe is weakly Tarski by equivalences, because both definitional equality of types A≡BA \equiv B and the identity types between two types A=BA = B imply that the two types of equivalent A≃ 𝒰BA \simeq_\mathcal{U} B. Similarly, every strict Tarski universe is weakly Tarski by the identity type, because definitional equality of types A≡BA \equiv B implies that two types are identified A=BA = B.

Since each type former is independent of each other, one could also have mixed versions of Tarski universes, where some of the type formers are strictly Tarski and some are weakly Tarski. This leads to 2 n2^n possible Tarski universes, where nn is the number of type formers in a type theory, and the 2 n2^n type theories are only partially ordered by generality. Internally in an ambient universe, that number becomes 3 n3^n.

Universes defined internally via induction-recursion are stricty Tarski. Weakly Tarski universes are easier to obtain in semantics (see below): they are somewhat more annoying to use, but probably suffice for most purposes. In objective type theory, there is no definitional equality, so every Tarski universe is weakly Tarski.

Other universes

There are other universes which one could use. For example, any model of material set theory VV or structural set theory ℰ\mathcal{E} would suffice. Material set theories become Tarski universes by the type family

x:V⊢El(x)≔∑ y:Vy∈xx:V \vdash \mathrm{El}(x) \coloneqq \sum_{y:V} y \in x

and structural set theories become Tarski universes by the type family

x:V⊢El(x)≔hom(1,x)x:V \vdash \mathrm{El}(x) \coloneqq \mathrm{hom}(1, x)

where 1:ℰ1:\mathcal{E} is the terminal separator.

Thus, in a dependent type theory with a separate type judgment, one could simply include inference rules for ZFC or ETCS.

Properties

Universe enlargement

Both Coq and Agda support universe polymorphism to deal with the issue of universe enlargement. Moreover, Coq supports typical ambiguity.

Extensionality principle of type universes

The extensionality principle of type universes is given by the univalence axiom, which for Tarski universes (U,T)(U, T) states that transport across the universal type family TT is an equivalence of types for all small types A:UA:U and B:UB:U; and for Russell universes UU states that the recursively defined function idToEquiv\mathrm{idToEquiv}, which takes identifications between small types A:UA:U and B:UB:U to equivalences between AA and BB, is an equivalence of types for all small types A:UA:U and B:UB:U.

Cumulativity

A tower of universes is cumulative if A:𝒰 iA:\mathcal{U}_i implies A:𝒰 i+1A:\mathcal{U}_{i+1} (rather than, say, Lift(A):𝒰 i+1Lift(A):\mathcal{U}_{i+1}).

Cumulative Russell universes have some issues; see for instance Luo 12.

  • Coq uses Russell style universes. For practical purposes, it also has cumulativity, although there is some question (perhaps mainly semantic) of whether this is true internally or whether it uses casts that are simply hidden from the user.

  • Agda uses non-cumulative Russell style universes.

  • UFP13 (first edition) uses cumulative Russell style universes.

Categorical semantics

UnivalentRussell universes have been shown to be interpreted in type-theoretic model categories presenting the base (∞,1)-topos ∞Grpd (Kapulkin-Lumsdaine-Voevodsky 12)

and more generally presenting (∞,1)-toposes of (∞,1)-presheaves over elegant Reedy categories (Shulman 13).

Discussion for general (∞,1)-toposes (of (∞,1)-sheaves) that should have implementation weakly Tarski (Gallozzi 14, p. 49-50) is in (Gepner-Kock 12).

For more on this see the respective sections at relation between type theory and category theory.

Other types of types

There is other notions of type of types. Suppose we have a Russell universe UU or a Tarski universe (U,T)(U, T) and a function P:U→Prop UP:U \to \mathrm{Prop}_U. Then the type of UU-small types which satisfy PP is given by the dependent sum type ∑ A:UP(A)\sum_{A:U} P(A) for Russell universes and ∑ A:UT(P(A))\sum_{A:U} T(P(A)) for Tarski universes.

Since universes are internal models of type theory, in a dependent type theory with a separate type judgment, one could generalize the above notion of “type of UU-small types which satisfy PP” to the notion of “type of all types which satisfy PP”. Types AA, previously elements of the universe A:UA:U, are now judged to be types AtypeA \; \mathrm{type}. The function P:U→Prop UP:U \to \mathrm{Prop}_U which takes types to propositons is now an operator on types, which is defined using inference rules:

Γ⊢AtypeΓ⊢P(A)typeΓ⊢AtypeΓ⊢proptrunc P(A):isProp(P(A))type\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash P(A) \; \mathrm{type}} \quad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{proptrunc}_{P(A)}:\mathrm{isProp}(P(A)) \; \mathrm{type}}

Examples of such PP definable from the existing type formers in dependent type theory include

The resulting type of types which satisfy PP is denoted by Type P\mathrm{Type}_P.

Care must be taken for which PP one could use to define the type of all types which satisfy PP. For example, given unit type 𝟙\mathbb{1}, for P(A)≡A→𝟙P(A) \equiv A \to \mathbb{1} and P(A)≡isSet(A)P(A) \equiv \mathrm{isSet}(A), the resulting Type P\mathrm{Type}_P always contains itself or its set truncation in addition to the empty type, resulting in Girard's paradox; thus, one cannot form such types of types in the type theory. Similarly, for

P(A)≡∏ x:A∏ y:A(x= Ay)∨¬(x= Ay)P(A) \equiv \prod_{x:A} \prod_{y:A} (x =_A y) \vee \neg (x =_A y)

the resulting Type P\mathrm{Type}_P contains its set truncation in addition to the empty type if the principle of excluded middle holds for all propositions, resulting in Girard's paradox; thus, one could only form Type P\mathrm{Type}_P for

P(A)≡∏ x:A∏ y:A(x= Ay)∨¬(x= Ay)P(A) \equiv \prod_{x:A} \prod_{y:A} (x =_A y) \vee \neg (x =_A y)

if one doesn’t have excluded middle in the type theory.

Now, supposing that the dependent type theory has the above rules for P(A)P(A), Type P\mathrm{Type}_P could be presented either as a Russell universe or a Tarski universe in a dependent type theory. The difference between the two is that in the former, every type which satisfies PP in the type theory is literally an element of the type of types which satisfy PP, while in the latter, elements of Type P\mathrm{Type}_P are only indices of a type family El\mathrm{El}; every finite type in the type theory is only essentially Type P \mathrm{Type}_P -small for weak Tarski universes or judgmentally equal to an P(A)P(A) for A:Type PA:\mathrm{Type}_P for strict Tarski universes.

For weak Tarski type of types with satisfy PP, one also needs the typal congruence rules for forming P(A)P(A):

Γ⊢AtypeΓ⊢BtypeΓ⊢e:A≃BΓ⊢congform P(e):P(A)≃P(B)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash e:A \simeq B}{\Gamma \vdash \mathrm{congform}_P(e):P(A) \simeq P(B) \; \mathrm{type}}

As a strict Tarski universe

As a strict Tarski universe, the type of all types which satisfy PP is given by the following natural deduction inference rules:

Formation rules for the type of all types which satisfy PP:

ΓctxΓ⊢Type Ptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Type}_P \; \mathrm{type}}

Introduction rules for the type of all types which satisfy PP:

Γ⊢AtypeΓ⊢toElem A:P(A)→Type P\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toElem}_A:P(A) \to \mathrm{Type}_P}

Elimination rules for the type of all types which satisfy PP:

Γ⊢A:Type PΓ⊢El(A)typeΓ⊢A:Type PΓ⊢witn P(A):P(El(A))\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{witn}_P(A):P(\mathrm{El}(A))}

Computation rules for the type of all types which satisfy PP:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢El(toElem A(p))≡Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \mathrm{El}(\mathrm{toElem}_A(p)) \equiv A \; \mathrm{type}}

  • Judgmental computation rules:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢witn P(toElem A(p))≡p:P(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \mathrm{witn}_P(\mathrm{toElem}_A(p)) \equiv p:P(A)}

  • Typal computation rules:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢β Type P Witn P,A(p):witn P(toElem A(p))= P(A)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \beta_{\mathrm{Type}_P}^{\mathrm{Witn}_P,A}(p):\mathrm{witn}_P(\mathrm{toElem}_A(p)) =_{P(A)} p}

Uniqueness rules for the type of all types which satisfy PP:

  • Judgmental computation rules:

    Γ⊢A:Type PΓ⊢toElem El(A)(witn P(A))≡A:Type P\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{toElem}_{\mathrm{El}(A)}(\mathrm{witn}_P(A)) \equiv A:\mathrm{Type}_P}

  • Typal computation rules:

    Γ⊢A:Type PΓ⊢η Type P(A):toElem El(A)(witn P(A))= Type PA\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \eta_{\mathrm{Type}_P}(A):\mathrm{toElem}_{\mathrm{El}(A)}(\mathrm{witn}_P(A)) =_{\mathrm{Type}_P} A}

Extensionality principle of the type of all types which satisfy PP:

Γ⊢A:Type PΓ⊢B:Type PΓ⊢ext Type P(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{Type}_P \quad \Gamma \vdash B:\mathrm{Type}_P} {\Gamma \vdash \mathrm{ext}_{\mathrm{Type}_P}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}

As a weak Tarski universe

As a weak Tarski universe, the type of all types which satisfy PP is given by the following natural deduction inference rules:

Formation rules for the type of all types which satisfy PP:

ΓctxΓ⊢Type Ptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Type}_P \; \mathrm{type}}

Introduction rules for the type of all types which satisfy PP:

Γ⊢AtypeΓ⊢toElem A:P(A)→Type P\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toElem}_A:P(A) \to \mathrm{Type}_P}

Elimination rules for the type of all types which satisfy PP:

Γ⊢A:Type PΓ⊢El(A)typeΓ⊢A:Type PΓ⊢witn P(A):P(El(A))\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{witn}_P(A):P(\mathrm{El}(A))}

Computation rules for the type of all types which satisfy PP:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢β Type P El,A(p):El(toElem A(p))≃Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \beta_{\mathrm{Type}_P}^{\mathrm{El}, A}(p):\mathrm{El}(\mathrm{toElem}_A(p)) \simeq A \; \mathrm{type}}

  • Judgmental computation rules:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢congform P(β Type P El,A(p))(witn P(toElem A(p)))≡p:P(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \mathrm{congform}_P(\beta_{\mathrm{Type}_P}^{\mathrm{El}, A}(p))(\mathrm{witn}_P(\mathrm{toElem}_A(p))) \equiv p:P(A)}

  • Typal computation rules:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢β Type P witn P,A(p):congform P(β Type P El,A(p))(witn P(toElem A(p)))= P(A)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \beta_{\mathrm{Type}_P}^{\mathrm{witn}_P,A}(p):\mathrm{congform}_P(\beta_{\mathrm{Type}_P}^{\mathrm{El}, A}(p))(\mathrm{witn}_P(\mathrm{toElem}_A(p))) =_{P(A)} p}

where the equivalence

congform P(β Type P El,A(p)):P(El(toElem A(p)))≃P(A)\mathrm{congform}_P(\beta_{\mathrm{Type}_P}^{\mathrm{El}, A}(p)):P(\mathrm{El}(\mathrm{toElem}_A(p))) \simeq P(A)

is provided from the typal computation rules for P(A)P(A).

Uniqueness rules for the type of all types which satisfy PP:

  • Judgmental computation rules:

    Γ⊢A:Type PΓ⊢A≡toElem El(A)(witn P(A)):Type P\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash A \equiv \mathrm{toElem}_{\mathrm{El}(A)}(\mathrm{witn}_P(A)):\mathrm{Type}_P}

  • Typal computation rules:

    Γ⊢A:Type PΓ⊢η Type P(A):A= Type PtoElem El(A)(witn P(A))\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \eta_{\mathrm{Type}_P}(A):A =_{\mathrm{Type}_P} \mathrm{toElem}_{\mathrm{El}(A)}(\mathrm{witn}_P(A))}

Extensionality principle of the type of all types which satisfy PP:

Γ⊢A:Type PΓ⊢B:Type PΓ⊢ext Type P(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{Type}_P \quad \Gamma \vdash B:\mathrm{Type}_P} {\Gamma \vdash \mathrm{ext}_{\mathrm{Type}_P}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}

As a Russell universe

As a Russell universe, the type of all types which satisfy PP is given by the following natural deduction inference rules:

Formation rules for the type of all types which satisfy PP:

ΓctxΓ⊢Type Ptype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Type}_P \; \mathrm{type}}

Introduction rules for the type of all types which satisfy PP:

Γ⊢AtypeΓ⊢toElem A:P(A)→Type P\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toElem}_A:P(A) \to \mathrm{Type}_P}

Elimination rules for the type of all types which satisfy PP:

Γ⊢A:Type PΓ⊢AtypeΓ⊢A:Type PΓ⊢witn P(A):P(A)\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{witn}_P(A):P(A)}

Computation rules for the type of all types which satisfy PP:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢toElem A(p)≡Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \mathrm{toElem}_A(p) \equiv A \; \mathrm{type}}

  • Judgmental computation rules:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢witn P(toElem A(p))≡p:P(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \mathrm{witn}_P(\mathrm{toElem}_A(p)) \equiv p:P(A)}

  • Typal computation rules:

Γ⊢AtypeΓ⊢p:P(A)Γ⊢β Type P finWitn,A(p):witn P(toElem A(p))= P(A)p\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:P(A)}{\Gamma \vdash \beta_{\mathrm{Type}_P}^{\mathrm{finWitn},A}(p):\mathrm{witn}_P(\mathrm{toElem}_A(p)) =_{P(A)} p}

Uniqueness rules for the type of all types which satisfy PP:

  • Judgmental computation rules:

    Γ⊢A:Type PΓ⊢toElem A(witn P(A))≡A:Type P\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \mathrm{toElem}_{A}(\mathrm{witn}_P(A)) \equiv A:\mathrm{Type}_P}

  • Typal computation rules:

    Γ⊢A:Type PΓ⊢η Type P(A):toElem A(witn P(A))= Type PA\frac{\Gamma \vdash A:\mathrm{Type}_P}{\Gamma \vdash \eta_{\mathrm{Type}_P}(A):\mathrm{toElem}_{A}(\mathrm{witn}_P(A)) =_{\mathrm{Type}_P} A}

Extensionality principle of the type of all types which satisfy PP:

Γ⊢A:Type PΓ⊢B:Type PΓ⊢ext Type P(A,B):isEquiv(idToEquiv(A,B))\frac{\Gamma \vdash A:\mathrm{Type}_P \quad \Gamma \vdash B:\mathrm{Type}_P} {\Gamma \vdash \mathrm{ext}_{\mathrm{Type}_P}(A, B):\mathrm{isEquiv}(\mathrm{idToEquiv}(A, B))}

References

Type universes in Martin-Löf type theory originate in un-stratified and hence inconsistent form with

and then in stratified and consistent form in

  • Per Martin-Löf, §1.10 in: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80, Elsevier (1975) 73-118 [doi:10.1016/S0049-237X(08)71945-1, CiteSeer]

elaborated on in

which also introduces (p. 48) the distinction into notions of Russell universes and Tarski universes.

Further discussion in

Review and further discussion:

Introduction with an eye towards homotopy type theory:

Definition of weakly Tarski universes:

Detailed discussion of the type of types in Coq is in

See also around slide 8 of the survey

  • Frade, Calculus of inductive constructions (2008/2009) (pdf)

A formal proof in homotopy type theory that the type of homotopy n-types is not itself a homotopy nn-type (it is an (n+1)(n+1)-type) is in

(∞,1)-Categorical semantics for univalent type universes is discussed in

Relation to injective types:

See also

Last revised on May 23, 2024 at 14:21:28. See the history of this page for a list of all contributions to it.