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.

Categories with families

Categories with families, introduced by Dybjer, are a commonly used notion of model which stays relatively close to the syntax of type theory. They form a base substrate consisting of a substitution calculus, onto which extra structure is added for each type former supported by the type theory considered.

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}}_{\mathrm{\Gamma }}(A){)}_{A\in \mathrm{Ty}(\mathrm{\Gamma })}$ (we usually drop the subscript in ${\mathrm{Tm}}_{\mathrm{\Gamma }}(A)$). 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 \in \mathrm{Sub}(\mathrm{\Delta },\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 ]$. These operations are respectively called substitution in types and substitution in terms. The functoriality means that the following laws hold: $A[\sigma \circ \delta ]=A[\sigma ][\delta ]$, $A[\mathrm{i}\mathrm{d}]=A$, $t[\sigma \circ \delta ]=t[\sigma ][\delta ]$, $t[\mathrm{i}\mathrm{d}]=t$.
• 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 a certain presheaf on contexts, together with a natural isomorphism witnessing that this object represents it. This presheaf sends a context $\mathrm{\Delta }$ to the set of pairs of a substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$ and a term $t\in \mathrm{Tm}(A[\sigma ])$, and its action on a substitution $\delta \in \mathrm{Sub}(\mathrm{\Sigma },\mathrm{\Delta })$ is given by $(\sigma ,t)\mapsto (\sigma \circ \delta ,t[\delta ])$. The representing context is denoted $(\mathrm{\Gamma },A)$ and called the context extension of $\mathrm{\Gamma }$ by $A$. In one direction, the natural isomorphism sends a substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$ and a term $t\in \mathrm{Tm}(A[\sigma ])$ to a new substitution $(\sigma ,t)\in \mathrm{Sub}(\mathrm{\Delta },(\mathrm{\Gamma },A))$ called the substitution extension of $\sigma$ by $t$. In the other direction, it sends a substitution ${\sigma }^{\prime }\in \mathrm{Sub}(\mathrm{\Delta },(\mathrm{\Gamma },A))$ to a pair of its tail $\mathrm{tl}({\sigma }^{\prime })\in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$ and its head term $\mathrm{hd}(\sigma )\in \mathrm{Tm}(A[\mathrm{tl}({\sigma }^{\prime })])$. The fact that this is a natural isomorphism means that the following laws hold for $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$, $t\in \mathrm{Tm}(A[\sigma ])$, ${\sigma }^{\prime }\in \mathrm{Sub}(\mathrm{\Delta },(\mathrm{\Gamma },A))$, $\delta \in \mathrm{Sub}(\mathrm{\Sigma },\mathrm{\Delta })$:$$\begin{array}{rl}& \mathrm{tl}((\sigma ,t))=\sigma \\ & \mathrm{hd}((\sigma ,t))=t\\ & {\sigma }^{\prime }=(\mathrm{tl}({\sigma }^{\prime }),\mathrm{hd}({\sigma }^{\prime }))\\ & (\sigma ,t)\circ \delta =(\sigma \circ \delta ,t[\delta ])\\ & \mathrm{tl}({\sigma }^{\prime })\circ \delta =\mathrm{tl}({\sigma }^{\prime }\circ \delta )\\ & \mathrm{hd}({\sigma }^{\prime })[\delta ]=\mathrm{hd}({\sigma }^{\prime }\circ \delta )\end{array}$$

Given a context $\mathrm{\Gamma }\in \mathrm{Con}$ and a type $A\in \mathrm{Ty}(\mathrm{\Gamma })$, we define the weakening substitution ${\mathrm{w}\mathrm{k}}_{\mathrm{\Gamma },A}\in \mathrm{Sub}((\mathrm{\Gamma },A),\mathrm{\Gamma })$ by ${\mathrm{w}\mathrm{k}}_{\mathrm{\Gamma },A}:=\mathrm{tl}({\mathrm{i}\mathrm{d}}_{(\mathrm{\Gamma },A)})$, and the last variable ${\mathrm{vz}}_{\mathrm{\Gamma },A}\in {\mathrm{Tm}}_{(\mathrm{\Gamma },A)}(A[{\mathrm{wk}}_{\mathrm{\Gamma },A}])$ by ${\mathrm{vz}}_{\mathrm{\Gamma },A}:=\mathrm{hd}({\mathrm{i}\mathrm{d}}_{(\mathrm{\Gamma },A)})$. Observe that for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },(\mathrm{\Gamma },A))$, we have $$\mathrm{tl}(\sigma )=\mathrm{tl}({\mathrm{i}\mathrm{d}}_{(\mathrm{\Gamma },A)}\circ \sigma )=\mathrm{tl}({\mathrm{i}\mathrm{d}}_{(\mathrm{\Gamma },A)})\circ \sigma ={\mathrm{w}\mathrm{k}}_{\mathrm{\Gamma },A}\circ \sigma$$

Furthermore, given contexts $\mathrm{\Gamma },\mathrm{\Delta }\in \mathrm{Con}$, a substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$, and a type $A\in \mathrm{Ty}(\mathrm{\Gamma })$, we define a lifted substitution ${\sigma }^{+}\in \mathrm{Sub}((\mathrm{\Delta },A[\sigma ]),(\mathrm{\Gamma },A))$ by ${\sigma }^{+}:=(\sigma \circ {\mathrm{w}\mathrm{k}}_{\mathrm{\Gamma },A[\sigma ]},{\mathrm{vz}}_{\mathrm{\Delta },A[\sigma ]})$.

To interpret type formers, the following structures are added on top of a CwF.

For the unit type:

• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, a type ${\mathrm{\top }}_{\mathrm{\Gamma }}\in \mathrm{Ty}(\mathrm{\Gamma })$, with the requirement that ${\mathrm{\top }}_{\mathrm{\Gamma }}[\sigma ]={\mathrm{\top }}_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. (This can be replaced with a type in the empty context $\mathrm{\top }\in \mathrm{Ty}(\diamond )$, although the previous definition does not require the CwF to have a terminal object for the empty context.) This interprets the inference rule for type formation of the unit type in Martin-Löf type theory:$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\mathrm{\top }\text{type}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, a term ${\star }_{\mathrm{\Gamma }}\in \mathrm{Tm}({\mathrm{\top }}_{\mathrm{\Gamma }})$, with the requirement that ${\star }_{\mathrm{\Gamma }}[\sigma ]={\star }_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the introduction rule$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\star :\mathrm{\top }}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each type $C\in \mathrm{Ty}((\mathrm{\Gamma },{\mathrm{\top }}_{\mathrm{\Gamma }}))$, for each term $w\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},{\star }_{\mathrm{\Gamma }})])$, and for each term $t\in \mathrm{Tm}({\mathrm{\top }}_{\mathrm{\Gamma }})$, a term ${\mathrm{elim}}_{\mathrm{\top }}(\mathrm{\Gamma },C,w,t)\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},t)])$, with the requirement that ${\mathrm{elim}}_{\mathrm{\top }}(\mathrm{\Gamma },C,w,t)[\sigma ]={\mathrm{elim}}_{\mathrm{\top }}(\mathrm{\Delta },C[{\sigma }^{+}],w[\sigma ],t[\sigma ])$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the elimination rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathrm{\top }⊢C(x)\text{type}\mathrm{\Gamma }⊢w:C(\star )\mathrm{\Gamma }⊢t:\mathrm{\top }}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathrm{\top }}(C,w,t):C(t)}$$
• A requirement that ${\mathrm{elim}}_{\mathrm{\top }}(\mathrm{\Gamma },C,w,{\star }_{\mathrm{\Gamma }})=w$ for all context $\mathrm{\Gamma }\in \mathrm{Con}$, type $C\in \mathrm{Ty}((\mathrm{\Gamma },{\mathrm{\top }}_{\mathrm{\Gamma }}))$ and term $w\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},{\star }_{\mathrm{\Gamma }})])$. This interprets the computation rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathrm{\top }⊢C(x)\text{type}\mathrm{\Gamma }⊢w:C(\star )}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathrm{\top }}(C,w,\star )\equiv w}$$
• Optionally, a requirement that $t={\star }_{\mathrm{\Gamma }}$ for all context $\mathrm{\Gamma }$ and term $t\in \mathrm{Tm}({\mathrm{\top }}_{\mathrm{\Gamma }})$, if the type theory contains the uniqueness rule (η-rule)$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma }⊢t:\mathrm{\top }}{\mathrm{\Gamma }⊢t\equiv \star }$$

For the empty type:

• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, a type ${\mathrm{\perp }}_{\mathrm{\Gamma }}\in \mathrm{Ty}(\mathrm{\Gamma })$, with the requirement that ${\mathrm{\perp }}_{\mathrm{\Gamma }}[\sigma ]={\mathrm{\perp }}_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the type formation rule$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\mathrm{\perp }\text{type}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each type $C\in \mathrm{Ty}((\mathrm{\Gamma },{\mathrm{\perp }}_{\mathrm{\Gamma }}))$, for each term $f\in \mathrm{Tm}({\mathrm{\perp }}_{\mathrm{\Gamma }})$, a term ${\mathrm{elim}}_{\mathrm{\perp }}(\mathrm{\Gamma },C,t)\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},f)])$, with the requirement that ${\mathrm{elim}}_{\mathrm{\perp }}(\mathrm{\Gamma },C,f)[\sigma ]={\mathrm{elim}}_{\mathrm{\perp }}(\mathrm{\Delta },C[{\sigma }^{+}],f[\sigma ])$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the elimination rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathrm{\perp }⊢C(x)\text{type}\mathrm{\Gamma }⊢t:\mathrm{\perp }}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathrm{\perp }}(C,t):C(t)}$$

For the type of booleans:

• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, a type ${\mathbb{𝔹}}_{\mathrm{\Gamma }}\in \mathrm{Ty}(\mathrm{\Gamma })$, with the requirement that ${\mathbb{𝔹}}_{\mathrm{\Gamma }}[\sigma ]={\mathbb{𝔹}}_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the type formation rule$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\mathbb{𝔹}\text{type}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, terms ${\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}}_{\mathrm{\Gamma }},{\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}}_{\mathrm{\Gamma }}\in \mathrm{Tm}(\mathrm{\Gamma })$, with the requirement that ${\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}}_{\mathrm{\Gamma }}[\sigma ]={\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}}_{\mathrm{\Delta }}$ and ${\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}}_{\mathrm{\Gamma }}[\sigma ]={\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}}_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the introduction rules$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}:\mathbb{𝔹}}$$$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}:\mathbb{𝔹}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each type $C\in \mathrm{Ty}((\mathrm{\Gamma },{\mathbb{𝔹}}_{\mathrm{\Gamma }}))$, for each term $t\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},{\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}}_{\mathrm{\Gamma }})])$ and term $f\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},{\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}}_{\mathrm{\Gamma }})])$, and for each term $b\in \mathrm{Tm}({\mathbb{𝔹}}_{\mathrm{\Gamma }})$, a term ${\mathrm{elim}}_{\mathbb{𝔹}}(\mathrm{\Gamma },C,t,f,b)\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},b)])$, with the requirement that ${\mathrm{elim}}_{\mathbb{𝔹}}(\mathrm{\Gamma },C,t,f,b)[\sigma ]={\mathrm{elim}}_{\mathbb{𝔹}}(\mathrm{\Delta },C[{\sigma }^{+}],t[\sigma ],f[\sigma ],b[\sigma ])$ for all substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the elimination rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathbb{𝔹}⊢C(x)\text{type}\mathrm{\Gamma }⊢tC(\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e})\mathrm{\Gamma }⊢f:C(\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})\mathrm{\Gamma }⊢b:\mathbb{𝔹}}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathbb{𝔹}}(C,t,f,b):C(b)}$$
• A requirement that ${\mathrm{elim}}_{\mathbb{𝔹}}(\mathrm{\Gamma },C,t,f,{\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}}_{\mathrm{\Gamma }})=t$ and ${\mathrm{elim}}_{\mathbb{𝔹}}(\mathrm{\Gamma },C,t,f,{\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}}_{\mathrm{\Gamma }})=f$ for all context $\mathrm{\Gamma }\in \mathrm{Con}$, type $C\in \mathrm{Ty}((\mathrm{\Gamma },{\mathbb{𝔹}}_{\mathrm{\Gamma }}))$ and terms $t\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},{\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}}_{\mathrm{\Gamma }})])$ and $f\in \mathrm{Tm}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},{\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}}_{\mathrm{\Gamma }})])$. This interprets the computation rules$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathbb{𝔹}⊢C(x)\text{type}\mathrm{\Gamma }⊢t:C(\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e})\mathrm{\Gamma }⊢f:C(\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathbb{𝔹}}(C,t,f,\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e})\equiv t}$$$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathbb{𝔹}⊢C(x)\text{type}\mathrm{\Gamma }⊢t:C(\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e})\mathrm{\Gamma }⊢f:C(\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathbb{𝔹}}(C,t,f,\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})\equiv f}$$

For the type of natural numbers:

• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, a type ${\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}\in \mathrm{Ty}(\mathrm{\Gamma })$, with the requirement that ${\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}[\sigma ]={\mathbb{\mathbb{N}}}_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the type formation rule$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢\mathbb{\mathbb{N}}\text{type}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, a term $0_{\mathrm{\Gamma }}\in {\mathrm{Tm}}_{\mathrm{\Gamma }}$, with the requirement that $0_{\mathrm{\Gamma }}[\sigma ]=0_{\mathrm{\Delta }}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Gamma },\mathrm{\Delta })$; additionally, for each context $\mathrm{\Gamma }\in \mathrm{Con}$ and term $n\in \mathrm{Tm}({\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }})$, a term $S_{\mathrm{\Gamma }}(n)\in \mathrm{Tm}({\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }})$, with the requirement that $S_{\mathrm{\Gamma }}(n)[\sigma ]=S_{\mathrm{\Delta }}(n[\sigma ])$ for all substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the introduction rules$$\frac{\mathrm{\Gamma }\text{context}}{\mathrm{\Gamma }⊢0:\mathbb{\mathbb{N}}}$$$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma }⊢n:\mathbb{\mathbb{N}}}{\mathrm{\Gamma }⊢S(n):\mathbb{\mathbb{N}}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each type $C\in \mathrm{Ty}((\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}))$, for each term $z\in {\mathrm{Tm}}_{\mathrm{\Gamma }}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},0_{\mathrm{\Gamma }})])$ and term $s\in {\mathrm{Tm}}_{((\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}),C)}(C[({\mathrm{w}\mathrm{k}}_{(\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}),A}\circ {\mathrm{w}\mathrm{k}}_{\mathrm{\Gamma },\mathbb{\mathbb{N}}},S_{((\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}),A)}({\mathrm{vz}}_{\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}}[{\mathrm{wk}}_{(\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}),C}]))])$, and for each term $n\in {\mathrm{Tm}}_{\mathrm{\Gamma }}({\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }})$, a term ${\mathrm{elim}}_{\mathbb{\mathbb{N}}}(\mathrm{\Gamma },C,z,s,n)\in {\mathrm{Tm}}_{\mathrm{\Gamma }}(C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},n)])$, with the requirement that ${\mathrm{elim}}_{\mathbb{\mathbb{N}}}(\mathrm{\Gamma },C,z,s,n)[\sigma ]={\mathrm{elim}}_{\mathbb{\mathbb{N}}}(\mathrm{\Delta },C[{\sigma }^{+}],z[\sigma ],s[{\sigma }^{+}])$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the elimination rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathbb{\mathbb{N}}⊢C(x)\text{type}\mathrm{\Gamma }⊢z:C(0)\mathrm{\Gamma },m:\mathbb{\mathbb{N}},w:C(m)⊢s(m,w):C(S(m))\mathrm{\Gamma }⊢n:\mathbb{\mathbb{N}}}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathbb{\mathbb{N}}}(C,z,s,n):C(n)}$$
• A requirement that ${\mathrm{elim}}_{\mathbb{\mathbb{N}}}(\mathrm{\Gamma },C,z,s,0_{\mathrm{\Gamma }})=z$ for all $\mathrm{\Gamma }$, $C$, $z$, $s$ as above, and moreover that ${\mathrm{elim}}_{\mathbb{\mathbb{N}}}(\mathrm{\Gamma },C,z,s,S_{\mathrm{\Gamma }}(n))=s[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}},{\mathrm{elim}}_{\mathbb{\mathbb{N}}}(\mathrm{\Gamma },C,z,s,n)[{\mathrm{wk}}_{(\mathrm{\Gamma },{\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }}),C}])\circ ({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},n))$ when additionally $n\in \mathrm{Tm}({\mathbb{\mathbb{N}}}_{\mathrm{\Gamma }})$. This interprets the computation rules$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathbb{\mathbb{N}}⊢C(x)\text{type}\mathrm{\Gamma }⊢z:C(0)\mathrm{\Gamma },m:\mathbb{\mathbb{N}},w:C(m)⊢s(m,w):C(S(m))}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathbb{\mathbb{N}}}(C,z,s,0)\equiv z}$$$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma },x:\mathbb{\mathbb{N}}⊢C(x)\text{type}\mathrm{\Gamma }⊢z:C(0)\mathrm{\Gamma },m:\mathbb{\mathbb{N}},w:C(m)⊢s(m,w):C(S(m))n:\mathbb{\mathbb{N}}}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\mathbb{\mathbb{N}}}(C,z,s,S(n))\equiv S(n,{\mathrm{elim}}_{\mathbb{\mathbb{N}}}(C,z,s,n))}$$

For binary product types:

• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each types $A,B\in \mathrm{Ty}(\mathrm{\Gamma })$, a type $A{\times }_{\mathrm{\Gamma }}B\in \mathrm{Ty}(\mathrm{\Gamma })$, with the requirement that $(A{\times }_{\mathrm{\Gamma }}B)[\sigma ]=A[\sigma ]{\times }_{\mathrm{\Delta }}B[\sigma ]$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the type formation rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma }⊢A\text{type}\mathrm{\Gamma }⊢B\text{type}}{\mathrm{\Gamma }⊢A\times B\text{type}}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each types $A,B\in \mathrm{Ty}(\mathrm{\Gamma })$, for each term $a\in \mathrm{Tm}(A)$ and term $b\in \mathrm{Tm}(B)$, a term $⟨a,b{⟩}_{\mathrm{\Gamma },A,B}$, with the requirement that $⟨a,b{⟩}_{\mathrm{\Gamma },A,B}[\sigma ]=⟨a[\sigma ],b[\sigma ]{⟩}_{\mathrm{\Delta },A[\sigma ],B[\sigma ]}$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the introduction rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma }⊢A\text{type}\mathrm{\Gamma }⊢B\text{type}\mathrm{\Gamma }⊢a:A\mathrm{\Gamma }⊢b:B}{\mathrm{\Gamma }⊢⟨a,b⟩:A\times B}$$
• For each context $\mathrm{\Gamma }\in \mathrm{Con}$, for each types $A,B\in \mathrm{Ty}(\mathrm{\Gamma })$, for each type $C\in \mathrm{Ty}((\mathrm{\Gamma },A{\times }_{\mathrm{\Gamma }}B))$, for each term $w\in {\mathrm{Tm}}_{((\mathrm{\Gamma },A),B^{\prime })}(C[({\mathrm{wk}}_{(\mathrm{\Gamma },A),B^{\prime }}\circ {\mathrm{wk}}_{\mathrm{\Gamma },A},q)])$ where $B^{\prime }:=B[{\mathrm{wk}}_{\mathrm{\Gamma },A}]$, $A^{″}:=A[{\mathrm{wk}}_{(\mathrm{\Gamma },A),B^{\prime }}\circ {\mathrm{wk}}_{\mathrm{\Gamma },A}]$, $B^{″}:=B^{\prime }[{\mathrm{wk}}_{(\mathrm{\Gamma },A),B^{\prime }}]$, $q:=⟨{\mathrm{vz}}_{\mathrm{\Gamma },A}[{\mathrm{wk}}_{(\mathrm{\Gamma },A),B^{\prime }}],{\mathrm{vz}}_{(\mathrm{\Gamma },A),B^{\prime }}{⟩}_{((\mathrm{\Gamma },A),B^{\prime }),A^{″},B^{″}}$, for each term $p\in \mathrm{Tm}(A{\times }_{\mathrm{\Gamma }}B)$, a term ${\mathrm{elim}}_{\times }(\mathrm{\Gamma },A,B,C,w,p)\in C[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},p)]$, with the requirement that ${\mathrm{elim}}_{\times }(\mathrm{\Gamma },A,B,C,w,p)[\sigma ]={\mathrm{elim}}_{\times }(\mathrm{\Delta },A[\sigma ],B[\sigma ],C[{\sigma }^{+}],w[({\sigma }^{+}{)}^{+}],p[\sigma ])$ for every substitution $\sigma \in \mathrm{Sub}(\mathrm{\Delta },\mathrm{\Gamma })$. This interprets the elimination rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma }⊢A\text{type}\mathrm{\Gamma }⊢B\text{type}\mathrm{\Gamma },x:A\times B⊢C(x)\text{type}\mathrm{\Gamma },y:A,z:B⊢w(y,z):C(⟨y,z⟩)\mathrm{\Gamma }⊢p:A\times B}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\times }(A,B,C,w,p):C(p)}$$
• A requirement that ${\mathrm{elim}}_{\times }(\mathrm{\Gamma },A,B,C,w,⟨a,b{⟩}_{\mathrm{\Gamma },A,B})=w[({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma },A},b[{\mathrm{wk}}_{\mathrm{\Gamma },A}])\circ ({\mathrm{i}\mathrm{d}}_{\mathrm{\Gamma }},a)]$ for all $\mathrm{\Gamma }$, $A$, $B$, $w$ as above and $a\in \mathrm{Tm}(A)$, $b\in \mathrm{Tm}(B)$. This interprets the computation rule$$\frac{\mathrm{\Gamma }\text{context}\mathrm{\Gamma }⊢A\text{type}\mathrm{\Gamma }⊢B\text{type}\mathrm{\Gamma },x:A\times BC(x)\text{type}\mathrm{\Gamma },y:A,z:B⊢w(y,z):C(⟨y,z⟩)\mathrm{\Gamma }⊢a:A\mathrm{\Gamma }⊢b:B}{\mathrm{\Gamma }⊢{\mathrm{elim}}_{\times }(A,B,C,w,⟨a,b⟩\equiv w(a,b)}$$

Other kinds of models

Notions of models other than categories with families 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.