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 $\Gamma$ to $\Delta$ is denoted $\mathrm{Sub}(\Gamma ,\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 $\Gamma$ is denoted $(\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\Gamma )}$. The elements of $\mathrm{Ty}(\Gamma )$ are called types in context $\Gamma$, and the elements of $\mathrm{Tm}(A)$ are called terms of type $A$ (in context $\Gamma$). The image of a substitution $\sigma :\Delta \to \Gamma$ is a morphism $(\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\Gamma )}\to (\mathrm{Tm}(B){)}_{B\in \mathrm{Ty}(\Delta )}$ in $\mathrm{Fam}$. Its component $\mathrm{Ty}(\Gamma )\to \mathrm{Ty}(\Delta )$ is denoted by $A\mapsto A[\sigma ]$, and for each $A\in \mathrm{Ty}(\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 $\Gamma$ and for each type $A\in \mathrm{Ty}(\Gamma )$, a representing object for the presheaf on the slice category $\mathrm{Con}/\Gamma$ that sends a substitution $\sigma :\Delta \to \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 $(\Gamma ,A)$, called the extension of $\Gamma$ by $A$, along with a substitution ${\mathrm{wk}}_A:(\Gamma ,A)\to \Gamma$ called weakening. The natural isomorphism sends a substitution $\sigma :\Delta \to \Gamma$ and a term $t\in \mathrm{Tm}(A[\sigma ])$ to a substitution denoted $(\sigma ,t):\Delta \to (\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}{c}\\ 𝖢𝗈𝗇& :𝖲𝖾𝗍& & \text{(contexts)}\\ 𝖲𝗎𝖻& :𝖢𝗈𝗇\to 𝖢𝗈𝗇\to 𝖲𝖾𝗍& & \text{(substitutions)}\\ -\circ -& :\{\Gamma \Delta \Sigma :𝖢𝗈𝗇\}\to 𝖲𝗎𝖻\Delta \Gamma \to 𝖲𝗎𝖻\Sigma \Delta \to 𝖲𝗎𝖻\Sigma \Gamma & & \text{(composition of substitutions)}\\ 𝗂𝖽& :\{\Gamma :𝖢𝗈𝗇\}\to 𝖲𝗎𝖻\Gamma \Gamma & & \text{(identity substitution)}\\ & :(\Gamma \Delta \Sigma \Theta :𝖢𝗈𝗇)(\gamma :𝖲𝗎𝖻\Theta \Sigma )(\delta :𝖲𝗎𝖻\Sigma \Delta )(\sigma :𝖲𝗎𝖻\Delta \Gamma )\\ & \to (\sigma \circ \delta )\circ \gamma =\sigma \circ (\delta \circ \gamma )& & \text{(associativity of composition)}\\ & :(\Gamma \Delta :𝖢𝗈𝗇)\to (\sigma :𝖲𝗎𝖻\Delta \Gamma )\to \sigma \circ 𝗂𝖽=\sigma & & \text{(right identity law)}\\ & :(\Gamma \Delta :𝖢𝗈𝗇)\to (\sigma :𝖲𝗎𝖻\Delta \Gamma )\to 𝗂𝖽\circ \sigma =\sigma & & \text{(left identity law)}\\ 𝖳𝗒& :𝖢𝗈𝗇\to 𝖲𝖾𝗍& & \text{(types)}\\ 𝖳𝗆& :(\Gamma :𝖢𝗈𝗇)\to 𝖳𝗒\Gamma \to 𝖲𝖾𝗍& & \text{(terms)}\\ -[-]& :\{\Gamma \Delta :𝖢𝗈𝗇\}\to 𝖳𝗒\Gamma \to 𝖲𝗎𝖻\Delta \Gamma \to 𝖳𝗒\Delta & & \text{(substitution in types)}\\ -[-]& :\{\Gamma \Delta :𝖢𝗈𝗇\}\{A:𝖳𝗒\Gamma \}\to 𝖳𝗆A\to (\sigma :𝖲𝗎𝖻\Delta \Gamma )\to 𝖳𝗆A[\sigma ]& & \text{(substitution in terms)}\\ & :(\Gamma \Delta \Sigma :𝖢𝗈𝗇)(\delta :𝖲𝗎𝖻\Sigma \Delta )(\sigma :𝖲𝗎𝖻\Delta \Gamma )(A:𝖳𝗒\Gamma )\\ & \to A[\sigma \circ \delta ]=A[\sigma ][\delta ]& & \text{(functoriality of substitution in types)}\\ & :(\Gamma :𝖢𝗈𝗇)(A:𝖳𝗒\Gamma )\to A[𝗂𝖽]=A& & \text{(idem)}\\ & :(\Gamma \Delta \Sigma :𝖢𝗈𝗇)(\delta :𝖲𝗎𝖻\Sigma \Delta )(\sigma :𝖲𝗎𝖻\Delta \Gamma )(A:𝖳𝗒\Gamma )(t:𝖳𝗆A)\\ & \to t[\sigma \circ \delta ]=t[\sigma ][\delta ]& & \text{(functoriality of substitution in terms)}\\ & :(\Gamma :𝖢𝗈𝗇)(A:𝖳𝗒\Gamma )(t:𝖳𝗆A)\to t[𝗂𝖽]=t& & \text{(idem)}\\ \diamond & :𝖢𝗈𝗇& & \text{(empty context)}\\ \epsilon & :(\Gamma :𝖢𝗈𝗇)\to 𝖲𝗎𝖻\Gamma \diamond & & \text{(substitution to the empty context)}\\ & :(\Gamma :𝖢𝗈𝗇)(\sigma :𝖲𝗎𝖻\Gamma \diamond )\to \sigma =\epsilon \Gamma & & \text{(uniqueness of substitution to the empty context)}\\ (-,-)& :(\Gamma :𝖢𝗈𝗇)\to 𝖳𝗒\Gamma \to 𝖢𝗈𝗇& & \text{(context extension)}\\ 𝗐𝗄& :\{\Gamma :𝖢𝗈𝗇\}\{A:𝖳𝗒\Gamma \}\to 𝖲𝗎𝖻(\Gamma ,A)\Gamma & & \text{(weakening)}\\ (-,-)& :\{\Gamma \Delta :𝖢𝗈𝗇)\{A:𝖳𝗒\Gamma \}\\ & \to (\sigma :𝖲𝗎𝖻\Delta \Gamma )\to 𝖳𝗆A[\sigma ]\to 𝖲𝗎𝖻\Delta (\Gamma ,A)& & \text{(substitution extension)}\\ & :(\Gamma \Delta \Sigma 𝖢𝗈𝗇)(\sigma :𝖲𝗎𝖻\Delta \Gamma )(\delta :𝖲𝗎𝖻\Sigma \Delta )(A:𝖳𝗒\Gamma )(t:𝖳𝗆A[\sigma ])\\ & \to (\sigma ,t)\circ \delta =(\sigma \circ \delta ,t[\delta ])& & \text{(naturality of substitution extension)}\\ 𝗁𝖽& :\{\Gamma \Delta :𝖢𝗈𝗇)\{A:𝖳𝗒\Gamma \}\to (\sigma :𝖲𝗎𝖻\Delta (\Gamma ,A))\to 𝖳𝗆A[𝗐𝗄\circ \sigma ]& & \text{(head term of a substitution)}\\ & :(\Gamma \Delta \Sigma :𝖢𝗈𝗇)(A:𝖳𝗒\Gamma )(\sigma :𝖲𝗎𝖻\Delta \Gamma )(\delta :𝖲𝗎𝖻\Sigma \Delta )\\ & \to 𝗁𝖽(\sigma \circ \delta )=(𝗁𝖽\sigma )[\delta ]& & \text{(naturality of head)}\\ & :(\Gamma \Delta :𝖢𝗈𝗇)(A:𝖳𝗒\Gamma )(\sigma :𝖲𝗎𝖻\Delta (\Gamma ,A))\to \sigma =(𝗐𝗄\circ \sigma ,𝗁𝖽\sigma )& & \text{(head is inverse to substitution extension)}\\ & :(\Gamma \Delta :𝖢𝗈𝗇)(A:𝖳𝗒\Gamma )(\sigma :𝖲𝗎𝖻\Delta \Gamma )(t:𝖳𝗆A[\sigma ])\to 𝗁𝖽(\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.