Semantics of type theory

The semantics of type theory involves several closely related types of models, which are constructed and studied in order to justify axioms and new type theories, and to use type theory as an internal language for categories, higher categories and other mathematical structures.

Types of models

Categories with families

Let $\mathrm{Fam}$ denote the category of families of sets: an object is a family $(A_i{)}_{i\in I}$ where each $A_i$ is a set, and a morphism $f:(A_i{)}_{i\in I}\to (B_j{)}_{j\in J}$ is a function $r:I\to J$ together with, for each $i\in I$, a function $t_i:A_i\to B_{r(i)}$. (This category is equivalent to the arrow category ${\mathrm{Set}}^{\to }$ of $\mathrm{Set}$ through the functor that sends a function $f:A\to I$ to the family $(f^{-1}(i){)}_{i\in I}$, with the natural action on morphisms.)

A category with families (CwF) consists of the following data:

• A category, whose class of objects is denoted $\mathrm{Con}$ and whose class of morphisms from $\mathrm{\Gamma }$ to $\mathrm{\Delta }$ is denoted $\mathrm{Sub}(\mathrm{\Gamma },\mathrm{\Delta })$. The objects are called contexts and the morphisms are called substitutions.
• A contravariant functor from the category of contexts to $\mathrm{Fam}$. The image of a context $\mathrm{\Gamma }$ is denoted $(\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\mathrm{\Gamma })}$. The elements of $\mathrm{Ty}(\mathrm{\Gamma })$ are called types in context $\mathrm{\Gamma }$, and the elements of $\mathrm{Tm}(A)$ are called terms of type $A$ (in context $\mathrm{\Gamma }$). The image of a substitution $\sigma :\mathrm{\Delta }\to \mathrm{\Gamma }$ is a morphism $(\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\mathrm{\Gamma })}\to (\mathrm{Tm}(B){)}_{B\in \mathrm{Ty}(\mathrm{\Delta })}$ in $\mathrm{Fam}$. Its component $\mathrm{Ty}(\mathrm{\Gamma })\to \mathrm{Ty}(\mathrm{\Delta })$ is denoted by $A\mapsto A[\sigma ]$, and for each $A\in \mathrm{Ty}(\mathrm{\Gamma })$, its component $\mathrm{Tm}(A)\to \mathrm{Tm}(A[\sigma ])$ is also denoted $t\mapsto t[\sigma ]$.
• A terminal object in the category of contexts, called the empty context and denoted $\diamond$. (Some authors omit this requirement.)
• For each context $\mathrm{\Gamma }$ and for each type $A\in \mathrm{Ty}(\mathrm{\Gamma })$, a representing object for the presheaf on the slice category $\mathrm{Con}/\mathrm{\Gamma }$ that sends a substitution $\sigma :\mathrm{\Delta }\to \mathrm{\Gamma }$ to the set $\mathrm{Tm}(A[\sigma ])$ (with action on a morphism $\delta$ given by $-[\delta ]:\mathrm{Tm}(A[\sigma ])\to \mathrm{Tm}(A[\sigma \circ \delta ])$), along with a natural isomorphism witnessing that this object represents the presheaf. This representing object consists of a context denoted $(\mathrm{\Gamma },A)$, called the extension of $\mathrm{\Gamma }$ by $A$, along with a substitution ${\mathrm{wk}}_A:(\mathrm{\Gamma },A)\to \mathrm{\Gamma }$ called weakening. The natural isomorphism sends a substitution $\sigma :\mathrm{\Delta }\to \mathrm{\Gamma }$ and a term $t\in \mathrm{Tm}(A[\sigma ])$ to a substitution denoted $(\sigma ,t):\mathrm{\Delta }\to (\mathrm{\Gamma },A)$, called the extension of $\sigma$ by $t$.

Fully unfolding the requirements results in the following presentation of CwFs as a generalized algebraic theory. (The notation $(x:A)\to B(x)$ stands for the dependent product $\prod _{x:A}B(x)$, and curly braces denote arguments which are left implicit for readability.)

$$\begin{array}{r}\\ \mathsf{C}\mathsf{o}\mathsf{n}& :\mathsf{S}\mathsf{e}\mathsf{t}& & \text{(contexts)}\\ \mathsf{S}\mathsf{u}\mathsf{b}& :\mathsf{C}\mathsf{o}\mathsf{n}\to \mathsf{C}\mathsf{o}\mathsf{n}\to \mathsf{S}\mathsf{e}\mathsf{t}& & \text{(substitutions)}\\ -\circ -& :\{\mathrm{\Gamma }\mathrm{\Delta }\mathrm{\Sigma }:\mathsf{C}\mathsf{o}\mathsf{n}\}\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma }\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Delta }\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Gamma }& & \text{(composition of substitutions)}\\ \mathsf{i}\mathsf{d}& :\{\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n}\}\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Gamma }\mathrm{\Gamma }& & \text{(identity substitution)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }\mathrm{\Sigma }\mathrm{\Theta }:\mathsf{C}\mathsf{o}\mathsf{n})(\gamma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Theta }\mathrm{\Sigma })(\delta :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Delta })(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })\\ & \to (\sigma \circ \delta )\circ \gamma =\sigma \circ (\delta \circ \gamma )& & \text{(associativity of composition)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n})\to (\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })\to \sigma \circ \mathsf{i}\mathsf{d}=\sigma & & \text{(right identity law)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n})\to (\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })\to \mathsf{i}\mathsf{d}\circ \sigma =\sigma & & \text{(left identity law)}\\ \mathsf{T}\mathsf{y}& :\mathsf{C}\mathsf{o}\mathsf{n}\to \mathsf{S}\mathsf{e}\mathsf{t}& & \text{(types)}\\ \mathsf{T}\mathsf{m}& :(\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n})\to \mathsf{T}\mathsf{y}\mathrm{\Gamma }\to \mathsf{S}\mathsf{e}\mathsf{t}& & \text{(terms)}\\ -[-]& :\{\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n}\}\to \mathsf{T}\mathsf{y}\mathrm{\Gamma }\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma }\to \mathsf{T}\mathsf{y}\mathrm{\Delta }& & \text{(substitution in types)}\\ -[-]& :\{\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n}\}\{A:\mathsf{T}\mathsf{y}\mathrm{\Gamma }\}\to \mathsf{T}\mathsf{m}A\to (\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })\to \mathsf{T}\mathsf{m}A[\sigma ]& & \text{(substitution in terms)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }\mathrm{\Sigma }:\mathsf{C}\mathsf{o}\mathsf{n})(\delta :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Delta })(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })\\ & \to A[\sigma \circ \delta ]=A[\sigma ][\delta ]& & \text{(functoriality of substitution in types)}\\ & :(\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n})(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })\to A[\mathsf{i}\mathsf{d}]=A& & \text{(idem)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }\mathrm{\Sigma }:\mathsf{C}\mathsf{o}\mathsf{n})(\delta :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Delta })(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })(t:\mathsf{T}\mathsf{m}A)\\ & \to t[\sigma \circ \delta ]=t[\sigma ][\delta ]& & \text{(functoriality of substitution in terms)}\\ & :(\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n})(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })(t:\mathsf{T}\mathsf{m}A)\to t[\mathsf{i}\mathsf{d}]=t& & \text{(idem)}\\ \diamond & :\mathsf{C}\mathsf{o}\mathsf{n}& & \text{(empty context)}\\ \epsilon & :(\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n})\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Gamma }\diamond & & \text{(substitution to the empty context)}\\ & :(\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n})(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Gamma }\diamond )\to \sigma =\epsilon \mathrm{\Gamma }& & \text{(uniqueness of substitution to the empty context)}\\ (-,-)& :(\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n})\to \mathsf{T}\mathsf{y}\mathrm{\Gamma }\to \mathsf{C}\mathsf{o}\mathsf{n}& & \text{(context extension)}\\ \mathsf{w}\mathsf{k}& :\{\mathrm{\Gamma }:\mathsf{C}\mathsf{o}\mathsf{n}\}\{A:\mathsf{T}\mathsf{y}\mathrm{\Gamma }\}\to \mathsf{S}\mathsf{u}\mathsf{b}(\mathrm{\Gamma },A)\mathrm{\Gamma }& & \text{(weakening)}\\ (-,-)& :\{\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n})\{A:\mathsf{T}\mathsf{y}\mathrm{\Gamma }\}\\ & \to (\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })\to \mathsf{T}\mathsf{m}A[\sigma ]\to \mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }(\mathrm{\Gamma },A)& & \text{(substitution extension)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }\mathrm{\Sigma }\mathsf{C}\mathsf{o}\mathsf{n})(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })(\delta :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Delta })(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })(t:\mathsf{T}\mathsf{m}A[\sigma ])\\ & \to (\sigma ,t)\circ \delta =(\sigma \circ \delta ,t[\delta ])& & \text{(naturality of substitution extension)}\\ \mathsf{h}\mathsf{d}& :\{\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n})\{A:\mathsf{T}\mathsf{y}\mathrm{\Gamma }\}\to (\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }(\mathrm{\Gamma },A))\to \mathsf{T}\mathsf{m}A[\mathsf{w}\mathsf{k}\circ \sigma ]& & \text{(head term of a substitution)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }\mathrm{\Sigma }:\mathsf{C}\mathsf{o}\mathsf{n})(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })(\delta :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Sigma }\mathrm{\Delta })\\ & \to \mathsf{h}\mathsf{d}(\sigma \circ \delta )=(\mathsf{h}\mathsf{d}\sigma )[\delta ]& & \text{(naturality of head)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n})(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }(\mathrm{\Gamma },A))\to \sigma =(\mathsf{w}\mathsf{k}\circ \sigma ,\mathsf{h}\mathsf{d}\sigma )& & \text{(head is inverse to substitution extension)}\\ & :(\mathrm{\Gamma }\mathrm{\Delta }:\mathsf{C}\mathsf{o}\mathsf{n})(A:\mathsf{T}\mathsf{y}\mathrm{\Gamma })(\sigma :\mathsf{S}\mathsf{u}\mathsf{b}\mathrm{\Delta }\mathrm{\Gamma })(t:\mathsf{T}\mathsf{m}A[\sigma ])\to \mathsf{h}\mathsf{d}(\sigma ,t)=t& & \text{(idem)}\end{array}$$

Other

Other notions of models include comprehension categories, categories with attributes and contextual categories.

Main models

Models of type theory include the standard model (or set model),, the term model (or syntactic model, or initial model),, the setoid model, the groupoid model, the simplicial set model, and several models in cubical sets starting with the BCH (Bezem–Coquand–Huber) model.