of all homotopy types
|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination? for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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 of types a judgement of the form
says that is an -dependent type.
In homotopy type theory the type of types 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 type of all types, which therefore in particular contained itself, i.e. one had . 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 types of types, with and , etc.
Thus, the type formers have rules saying which universe they belong to, such as:
We usually also have operations on the universe corresponding to (but not identical to) type formers, such as
with an equality . 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 à la Tarski universe.
We can give a slightly different definition of weakly à la Tarski universe using propositional equality and a larger universe. More precisely, we can consider two (or many) universes and with the usual rules for the relative reflection for any , a choice of weakly or strongly a la Tarski computational rules for the reflections and , and a computation rule for the relative reflection el of inside based on propositional equality, which gives us canonical elements of the identity types and similarly for the other type formers.
If the containing universe is univalent the two definitions turn out to coincide.
Universes defined internally via induction-recursion? are (strongly) à la Tarski. Weakly à la Tarski universes are easier to obtain in semantics (see below): they are somewhat more annoying to use, but probably suffice for most purposes.
Both Coq and Agda have systems to manage universe sizes and universe enlargement automatically; Agda’s is more advanced (universe polymorphism), whereas Coq’s is good enough for many purposes but tends to produce “universe inconsistencies” when working with univalence.
Univalent type universes à la Russell 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).
For more on this see the respective sections at relation between type theory and category theory.
Basic discussion of the syntax of type universes is in
Definition of type universes weakly à la Tarski is in
Detailed discussion of the type of types in Coq is in
See also around slide 8 of the survey