Thesemantics oftype 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 aninternal language forcategories,higher categories and other mathematical structures.

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

Acategory with families (CwF) consists of the following data:^[1][2][3]

• Acategory, whose class of objects is denoted${\displaystyle \mathrm{Con}}$ and whose class of morphisms from${\displaystyle \mathrm{\Gamma }}$ to${\displaystyle \mathrm{\Delta }}$ is denoted${\displaystyle \mathrm{Sub}(\mathrm{\Gamma },\mathrm{\Delta })}$. The objects are calledcontexts and the morphisms are calledsubstitutions.
• Acontravariant functor from the category of contexts to${\displaystyle \mathrm{Fam}}$. The image of a context${\displaystyle \mathrm{\Gamma }}$ is denoted${\displaystyle (\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\mathrm{\Gamma })}}$. The elements of${\displaystyle \mathrm{Ty}(\mathrm{\Gamma })}$ are calledtypes in context${\displaystyle \mathrm{\Gamma }}$, and the elements of${\displaystyle \mathrm{Tm}(A)}$ are calledterms of type${\displaystyle A}$ (in context${\displaystyle \mathrm{\Gamma }}$). The image of a substitution${\displaystyle \sigma :\mathrm{\Delta }\to \mathrm{\Gamma }}$ is a morphism${\displaystyle (\mathrm{Tm}(A){)}_{A\in \mathrm{Ty}(\mathrm{\Gamma })}\to (\mathrm{Tm}(B){)}_{B\in \mathrm{Ty}(\mathrm{\Delta })}}$ in${\displaystyle \mathrm{Fam}}$. Its component${\displaystyle \mathrm{Ty}(\mathrm{\Gamma })\to \mathrm{Ty}(\mathrm{\Delta })}$ is denoted by${\displaystyle A\mapsto A[\sigma ]}$, and for each${\displaystyle A\in \mathrm{Ty}(\mathrm{\Gamma })}$, its component${\displaystyle \mathrm{Tm}(A)\to \mathrm{Tm}(A[\sigma ])}$ is also denoted${\displaystyle t\mapsto t[\sigma ]}$.
• Aterminal object in the category of contexts, called theempty context and denoted${\displaystyle \diamond }$. (Some authors omit this requirement.^[4])
• For each context${\displaystyle \mathrm{\Gamma }}$ and for each type${\displaystyle A\in \mathrm{Ty}(\mathrm{\Gamma })}$, arepresenting object for thepresheaf on theslice category${\displaystyle \mathrm{Con}/\mathrm{\Gamma }}$ that sends a substitution${\displaystyle \sigma :\mathrm{\Delta }\to \mathrm{\Gamma }}$ to the set${\displaystyle \mathrm{Tm}(A[\sigma ])}$ (with action on a morphism${\displaystyle \delta }$ given by${\displaystyle -[\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${\displaystyle (\mathrm{\Gamma },A)}$, called theextension of${\displaystyle \mathrm{\Gamma }}$ by${\displaystyle A}$, along with a substitution${\displaystyle {\mathrm{wk}}_A:(\mathrm{\Gamma },A)\to \mathrm{\Gamma }}$ calledweakening. The natural isomorphism sends a substitution${\displaystyle \sigma :\mathrm{\Delta }\to \mathrm{\Gamma }}$ and a term${\displaystyle t\in \mathrm{Tm}(A[\sigma ])}$ to a substitution denoted${\displaystyle (\sigma ,t):\mathrm{\Delta }\to (\mathrm{\Gamma },A)}$, called theextension of${\displaystyle \sigma }$ by${\displaystyle t}$.

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

This sectionneeds expansion. You can help byadding to it.(November 2025)

Other notions of models include comprehension categories, categories with attributes and contextual categories.^[4]

This section is empty. You can help byadding to it.(November 2025)

This sectionneeds expansion. You can help byadding to it.(November 2025)

Models of type theory include the standard model (or set model),^[1][3], the term model (or syntactic model, or initial model),^[1][3], the setoid model,^{[citation needed]} the groupoid model,^[6] thesimplicial set model,^[7] and several models incubical sets starting with the BCH (Bezem–Coquand–Huber) model.^[8]

• Semantics
• Type theory
• Systems of formal logic

• Articles to be expanded from November 2025
• All articles to be expanded
• Articles with empty sections from November 2025
• All articles with empty sections
• All articles with unsourced statements
• Articles with unsourced statements from November 2025