Semantics of type theory

There are several ways to package the structure of a model of type theory, including categories with families, comprehension categories, categories with attributes and contextual categories. In all cases, a model is a base substrate, together with extra structure and requirements for each rule of the type theory under consideration.

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.

Introduction

The CwF structure is designed to closely parallel the syntax of type theory.

To each derivable syntactic judgment of the form “ $Γ$ is a context”, the semantics in a CwF associates an element $\hat{Γ}$ of a set of contexts denoted $Con$ .
To each derivable judgment “ $A$ is a type in context $Γ$ ” is associated an element $\hat{A}$ of a set of types in context $\hat{Γ}$ denoted $Ty (\hat{Γ})$ . (Here $\hat{A}$ depends on $Γ$ and not merely on $A$ although this dependency is dropped in the notation.)
To each derivable judgment “ $t$ is a term of type $A$ in context $Γ$ ” (usually denoted $Γ ⊢ t : A$ ) is associated an element $\hat{t}$ of a set of terms of type $\hat{A}$ in context $\hat{Γ}$ , denoted ${Tm}_{\hat{Γ}} (\hat{A})$ .

(The terminology may be confusing because the "terms" of the model need not be finite syntactic objects as in the traditional sense of "term" in mathematical logic, but merely constitute the semantics of the syntactic terms of the type theory. Some authors instead call them elements, or refer to semantic contexts, semantic types and semantic terms.)

The semantic interpretation of definitional equality is always actual equality in the model, so whenever a judgment “ $A$ and $B$ are definitionally equal types in context $Γ$ ” is derivable, the interpretation in the model must ensure $\hat{A} = \hat{B}$ , and whenever “ $t$ and $u$ are definitionally equal terms of type $A$ in context $Γ$ ” is derivable, the interpretation ensures $\hat{t} = \hat{u}$ .

A CwF contains operations to interpret contexts: a special element $⋄ \in Con$ to model the empty context, and a context extension operation $▹$ to model the addition of a new variable to a context.

The remaining data of CwFs serves to interpret the substitution operation necessitated by dependent types: if $f$ has the dependent function type $(x : A) \to B$ where $B$ is a term involving the variable $x$ , the application of $f$ to a term $t$ has the type $B [x := t]$ . CwFs use parallel substitutions, namely substitutions between entire contexts. If there were a judgment in the syntax which was directly interpreted by a substitution from $\hat{Γ}$ to $\hat{Δ}$ in the CwF, it would be “ $σ$ is a list of terms in context $Γ$ , one for each type in $Δ$ , having this type with the previous variables from $Δ$ substituted by the previous terms in the list” (e.g., a parallel substitution from $Γ$ to $x : A, y : B$ in the syntax would be a term $t$ of type $A$ in context $Γ$ and a term $u$ of type $B [x := t]$ in context $Γ$ ).

Definition

Let $Fam$ denote the category of families of sets. An object of $Fam$ is a family $(A_{i})_{i \in I}$ where $I$ is a set and each $A_{i}$ is a set. A morphism $f : (A_{i})_{i \in I} \to (B_{j})_{j \in J}$ in $Fam$ 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 of $Set$ , through the correspondence between a function $f : A \to I$ and the family of sets $(f^{- 1} ({i}))_{i \in I}$ .)

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

A category.
The class of objects is denoted $Con$ and the objects are called contexts. The class of morphisms from a context $Δ$ to a context $Γ$ is denoted $Sub (Δ, Γ)$ and these morphisms are called substitutions from $Δ$ to $Γ$ .
A contravariant functor from this category to $Fam$ .
The image of a context $Γ$ is a family of sets denoted $({Tm}_{Γ} (A))_{A \in Ty (Γ)}$ (we usually drop the subscript in ${Tm}_{Γ} (A)$ ). The elements of $Ty (Γ)$ are called types in context $Γ$ , and the elements of $Tm (A)$ are called terms of type $A$ (in context $Γ$ ).
The image of a substitution $σ \in Sub (Δ, Γ)$ is a morphism $(Tm (A))_{A \in Ty (Γ)} \to (Tm (B))_{B \in Ty (Δ)}$ in $Fam$ . Its component $Ty (Γ) \to Ty (Δ)$ is denoted by $A \mapsto A [σ]$ , and for each $A \in Ty (Γ)$ , its component $Tm (A) \to Tm (A [σ])$ is also denoted $t \mapsto t [σ]$ . These operations are respectively called substitution in types and substitution in terms.
Alternatively, this data can be packaged as a presheaf of types $Ty$ on the category of contexts, and a dependent presheaf of terms $Tm$ on the category of contexts over the presheaf of types.
A terminal object in the category of contexts.
It is denoted $⋄$ and called the empty context.
For each context $Γ$ and for each type $A \in Ty (Γ)$ , consider the presheaf on the category of contexts which sends a context $Δ$ to the set of pairs of a substitution $σ \in Sub (Δ, Γ)$ and a term $t \in {Tm}_{Δ} (A [σ])$ . The functorial action of the presheaf on a substitution $δ \in Sub (Σ, Δ)$ is given by $(σ, t) \mapsto (σ \circ δ, t [δ])$ . The last part of the CwF data is a representing object for this presheaf, together with a natural isomorphism witnessing the representation.
The representing context is denoted $Γ ▹ A$ and called the context extension of $Γ$ by $A$ .
In one direction, the natural isomorphism sends a substitution $σ \in Sub (Δ, Γ)$ and a term $t \in Tm (A [σ])$ to a new substitution $(σ ▹ t) \in Sub (Δ, Γ ▹ A)$ called the substitution extension of $σ$ by $t$ . In the other direction, it sends a substitution $σ^{'} \in Sub (Δ, Γ ▹ A)$ to a pair of its tail $tl (σ^{'}) \in Sub (Δ, Γ)$ and its head term $hd (σ^{'}) \in Tm (A [tl (σ^{'})])$ .
Explicitly, the fact that this is a natural isomorphism means that the following laws hold: $\begin{matrix} tl (σ ▹ t) = σ \\ hd (σ ▹ t) = t \\ σ^{'} = tl (σ^{'}) ▹ hd (σ^{'}) \\ (σ ▹ t) \circ δ = (σ \circ δ) ▹ t [δ] \\ tl (σ^{'}) \circ δ = tl (σ^{'} \circ δ) \\ hd (σ^{'}) [δ] = hd (σ^{'} \circ δ) \end{matrix}$

Defined operations

Let $Γ$ be a context and $A$ a type in $Γ$ . The head and tail of the identity substitution from $Γ ▹ A$ to itself are respectively a substitution $wk \in Sub (Γ ▹ A, Γ)$ called weakening, and a term $vz \in {Tm}_{Γ ▹ A} (A [wk])$ called the head variable. Informally, the weakening adds an unused variable to the context, and the head variable is the term given by the variable last declared in the context.

Observe that weakening and the head variable allow to recover the tail and head of any substitution $σ \in Sub (Δ, Γ ▹ A)$ by $tl (σ) = tl (i d \circ σ) = tl (i d) \circ σ = w k \circ σ$ and $hd (σ) = hd (id \circ σ) = hd (id) [σ] = vz [σ] .$

Furthermore, given a substitution $σ \in Sub (Δ, Γ)$ , and a type $A \in Ty (Γ)$ , we define a lifted substitution $σ^{+} \in Sub (Δ ▹ A [σ], Γ ▹ A)$ by $σ^{+} := (σ \circ w k) ▹ vz$ .

Extra structure for type formers

For each rule of a particular type theory, there is added structure and/or requirements on a CwF for it to model the type theory.

A rule which introduces a type or term former is interpreted by an operation returning a type or term of the CwF, which is required to commute with substitution. The latter requirement is necessary since substitution is defined recursively in the syntax, e.g., $(A \times B) [x := t]$ is $A [x := t] \times B [x := t]$ .
A rule adding definitional equalities is interpreted by a requirement that the operations on the CwF satisfy a corresponding equation.

To illustrate this, consider the case of dependent pair types (Σ-types). The type formation rule is

$\frac{Γ context Γ ⊢ A type Γ, x : A ⊢ B type}{Γ ⊢ (x : A) \times B type}$

The corresponding operation on a CwF is: for each $Γ \in Con$ , for each $A \in Ty (Γ)$ , and for each $B \in Ty (Γ ▹ A)$ , a type $Σ (A, B) \in Ty (Γ)$ . This operation is required to satisfy the substitution rule: for all substitution $σ \in Sub (Δ, Γ)$ and types $A \in Ty (Γ), B \in Ty (Γ ▹ A)$ , we must have $Σ (A, B) [σ] = Σ (A [σ], B [σ^{+}])$ .

The term formation rules for the pairing operation is:

$\frac{Γ context Γ ⊢ A type Γ, x : A ⊢ B type Γ ⊢ t : A Γ ⊢ u : B [x := t]}{Γ ⊢ ⟨ t, u ⟩ : (x : A) \times B}$

The corresponding operation on a CwF is: for each $Γ \in Con$ , $A \in Ty (Γ)$ , $B \in Ty (Γ ▹ A)$ , $t \in Tm (A)$ and $u \in Tm (B [id ▹ t])$ ), a term $⟨ t, u ⟩ \in Tm (Σ (A, B))$ . This must satisfy the substitution rule:

$⟨ t, u ⟩ [σ] = ⟨ t [σ], u [σ] ⟩ .$

This equation is meaningful because of the CwF laws and the substitution rule for $Σ$ . The left hand side is an element of $Σ (A, B) [σ]$ , which by the substitution rule for $Σ$ is equal to $Σ (A [σ], B [σ^{+}])$ . To see that the right hand side is in this set, one has to check that $u [σ]$ is in $B [σ^{+}] [id ▹ t [σ]]$ . This holds because $u [σ]$ is in $B [id ▹ t] [σ]$ and

$\begin{matrix} B [id ▹ t] [σ] \\ = B [(id ▹ t) \circ σ] \\ = B [(id \circ σ) ▹ t [σ]] \\ = B [σ ▹ t [σ]] \end{matrix}$

while

$\begin{matrix} B [σ^{+}] [id ▹ t [σ]] \\ = B [(σ \circ wk) ▹ vz] [id ▹ t [σ]] \\ = B [((σ \circ wk) ▹ vz) \circ (id ▹ t [σ])] \\ = B [((σ \circ wk) \circ (id ▹ t [σ])) ▹ vz [id ▹ t [σ]]] \\ = B [σ \circ (wk \circ (id ▹ t [σ])) ▹ vz [id ▹ t [σ]]] \\ = B [σ \circ tl (id ▹ t [σ]) ▹ hd (id ▹ t [σ])] \\ = B [(σ \circ id) ▹ t [σ]] \\ = B [σ ▹ t [σ]] . \end{matrix}$

Finally, the remaining rules for dependent pair types are the computation rules (or β-rules)

$\frac{Γ context Γ ⊢ A type Γ, x : A ⊢ B type Γ ⊢ t : A Γ ⊢ u : B [x := t]}{Γ ⊢ fst (⟨ t, u ⟩) \equiv t : A}$

$\frac{Γ context Γ ⊢ A type Γ, x : A ⊢ B type Γ ⊢ t : A Γ ⊢ u : B [x := t]}{Γ ⊢ snd (⟨ t, u ⟩) \equiv u : B [x := t]}$

and the uniqueness rule (or η-rule)

$\frac{Γ context Γ ⊢ A type Γ, x : A ⊢ B type Γ ⊢ p : (x : A) \times B}{Γ ⊢ p \equiv ⟨ fst (p), snd (p) ⟩ : (x : A) \times B}$

These are interpreted by requiring the following equations on the previous operations:

$fst (⟨ t, u ⟩) = t$ and $snd (⟨ t, u ⟩) = u$ (for $Γ \in Con$ , $A \in Ty (Γ)$ , $B \in Ty (Γ ▹ A)$ , $t \in Tm (A)$ , $u \in Tm (B [id ▹ t])$ ),
$p = ⟨ fst (p), snd (p) ⟩$ (for $Γ \in Con$ , $A \in Ty (Γ)$ , $B \in Ty (Γ ▹ A)$ , $p \in Tm (Σ (A, B))$ ).

Universes

The case of universes is somewhat special because it is common to define the syntax of type theory without a separate judgment for “ $A$ is a type in context $Γ$ ”, instead using “ $A$ is a term of type $U$ in context $Γ$ ”, i.e., $Γ ⊢ A : U_{n}$ , where $U_{n}$ is the $n$ -th universe (also denoted ${T y p e}_{n}$ , especially in proof assistants). This is called Russell universes. To give semantics to this kind of type theory, one needs to requirement in the CwF structure that the interpretation of both kinds of judgments in the semantics coincide.

First consider the simpler case of a single Russell universe $U$ containing itself (the syntax has the type in type rule that $U$ has type $U$ , which is inconsistent). The corresponding requirements on a CwF are:

For each context $Γ$ , a type $U \in Ty (Γ)$ (we leave the dependency on $Γ$ implicit to lighten the notation), with the substitution rule $U [σ] = U$ . (This is equivalent to the data of a single type in the empty context $U \in Ty (⋄)$ , the version in an arbitrary context $Γ$ being recovered as $U [ϵ]$ where $ϵ$ is the unique substitution from $Γ$ to $⋄$ .)
An equality of sets $Ty (Γ) = {Tm}_{Γ} (U)$ for every context $Γ$ .

For a hierarchy of universes $U_{0}$ , $U_{1}$ where $U_{n}$ has type $U_{n + 1}$ , …, there is a complication since types are stratified in the syntax and therefore must also be stratified in the semantics. This is treated using a slight variant of CwFs which consists of a category of contexts and substitutions, a terminal object for the empty context, and for each universe level $n$ , a functor from this category to families of sets, mapping a context $Γ$ to a family $Γ \mapsto ({Tm}_{Γ} (A))_{A \in {Ty}_{n} (Γ)}$ of types of level $n$ and terms of these types, equipped with an operation to extend the context with a type of level $n$ (giving for $A \in {Ty}_{n} (Γ)$ a bijection $Sub (Δ, Γ ▹_{n} A) ≅ (σ \in Sub (Δ, Γ)) \times {Tm}_{Δ} (A [σ])$ natural in $Δ$ ). One can then model universes with, for each level $n$ , types $U_{n} \in {Ty}_{n + 1} (Γ)$ with the substitution rule $U_{n} [σ] = U_{n}$ , and an equality of sets ${Ty}_{n} (Γ) = {Tm}_{Γ} (U_{n})$ .

A slightly weaker variant is Coquand universes, which require a bijection between the sets ${Ty}_{n} (Γ)$ and ${Tm}_{Γ} (U_{n})$ natural in $Γ$ , instead of an equality. This corresponds to a syntax with a primitive operation $El$ that takes an element of the universe $U$ (a “code” for a type) and gives an actual type, and another primitive operation $code$ that converts back a type into a code, with definitional equalities $code (El (t)) \equiv t$ and $El (code (A)) \equiv A$ . Coquand's original motivation for introducing this style of universes is that they are the most natural to construct in presheaf models.

Finally, an even weaker variant is Tarski universes, which only have the $El$ operation but not a $code$ operation, and which require, for each type former, a counterpart on the level of codes, e.g., an operation $- \times_{c} -$ on ${Tm}_{Γ} (U)$ with the definitional equality $El (t \times_{c} u) \equiv El (t) \times El (u)$ , etc.

Some type theories have universe cumulativity: a type in a universe is also automatically a type in all higher universes. This can be treated in various ways, including subset inclusions between the ${Ty}_{n} (Γ)$ , and several variants of lifting operations between universes.

Democracy

The basic intuition stemming from the syntax is that a context is a list of types $x_{0} : A_{0}, \dots, x_{k - 1} : A_{k - 1}$ , which is essentially equivalent to an iterated Σ-type $(x_{0} : A_{0}) \times \dots \times (x_{k - 2} : A_{k - 2}) \times A_{k - 1}$ . This is not true in all models, but it can be a useful property to consider.

A CwF is democratic when every context $Γ$ is isomorphic (in the category of contexts) to $⋄ ▹ A$ for some closed type $A$ (i.e., a type in the empty context $⋄$ ).

5 more chapters are free with a Lably account.

The set model

The set model, or standard model, is the simplest model of type theory. Every construct is simply interpreted by its metatheoretic counterpart: a term of a function type is a function, a term of a product type is a pair, etc. (This is akin to the usual Tarskian semantics of first-order logic. If one constructs it in type theory itself as a metatheory and one views type theory as a programming language, it is a metacircular interpreter.)

The CwF is defined as follows:

A context is a set and a substitution is a function (so the category of contexts and substitutions is the category of sets).
A type in $Γ$ is a family of sets $(A_{i})_{i \in Γ}$ , and a term of this type is a choice of an element $t_{i} \in A_{i}$ for each $i \in Γ$ . The action of a substitution $σ : Δ \to Γ$ on a type $(A_{i})_{i \in Γ}$ gives $(A_{σ (j)})_{j \in Δ}$ , and on a term $(t_{i} \in A_{i})_{i \in Γ}$ , it gives $(t_{σ (j)} \in A_{σ (j)})_{j \in Δ}$ .
The empty context is a fixed singleton set.
The extension of a context $Γ$ by a type $(A_{i})_{i \in Γ}$ is the type of pairs of an $i \in Γ$ and an element of $A_{i}$ . The tail and head of a substitution $Δ \to (Γ ▹ (A_{i})_{i \in Γ}), j \mapsto (i_{j}, a_{j})$ are given by $j \mapsto i_{j}$ and $j \mapsto a_{j}$ .

All type formers are defined “pointwise”. For example, the product $(A_{i})_{i \in Γ} \times (B_{i})_{i \in Γ}$ is defined as $(A_{i} \times B_{i})_{i \in Γ}$ , the pairing of terms $(t_{i} \in A_{i})_{i \in Γ}$ and $(u_{i} \in B_{i})_{i \in Γ}$ is $((t_{i}, u_{i}) \in A_{i} \times B_{i})_{i \in Γ}$ , etc. This model supports essentially any type former supported by the metatheory (with the exception of universes: the metatheory needs a stronger universe than the object theory contains, namely a universe large enough to contain all universes from the object theory, as is expected from Gödel's second incompleteness theorem). It can model the equality reflection rule of extensional type theory, but not univalence.

The syntactic model

The syntactic model (or term model) is given by the contexts, parallel substitutions, types and terms in the syntax of the type theory under consideration, with the operations induced by all type and term constructors of the type theory.

For “reasonable” type theories, the syntactic model is also the initial model, which means that it has a unique morphism into every other model. The notion of morphism between models is usually defined by presenting the definition of a model as a generalized algebraic theory (GAT) (which is like an algebraic theory but allowing dependent functions), and applying the standard definition of morphism between algebras of a GAT. The initiality means that the syntax can indeed be interpreted in every model as expected. Actually establishing this turns out to be very tedious. While Cartmell and Hofmann proved it for some standard type theories, initiality became a contentious point in the research community around 2015 when some researchers, notably Voevodsky, opined that it was not justified to treat it as established for different type theories without carefully adapting the proofs. Most researchers consider the issue to have been satisfactorily solved by Uemura's introduction of the logical framework of second-order generalized algebraic theories (SOGATs), which encompasses practically all existing type theories (the main exception being substructural type theories), and his proof of initiality of the syntactic model for any SOGAT.

Meanwhile, it has also become common to eschew the traditional syntactic presentation of type theory entirely and define the syntax as the initial model (which exists for any GAT). This approach is called intrinsic syntax. At this level of abstraction, it is possible to construct and study models and to use type theory as an internal language for them (treating the traditional terms merely as a notation for elements of the model). It is not possible to study properties of the concrete, extrinsic syntax such as subject reduction and confluence. However, remarkably, the two main syntactic properties of some type theories, canonicity and normalization, can be stated and proved entirely at this level.

Presheaf models

Let $C$ be a category. The presheaf category $\hat{C}$ is equipped with a canonical CwF structure as follows.

A type $A$ in context $Γ$ is a dependent presheaf on $C$ over $Γ$ . This means the following data:

For each object $x \in C$ , and for each element $i \in Γ (x)$ , a set $A (x)_{i}$ ,
For each morphism $f : x \to y$ in $C$ , and for each element $i \in Γ (y)$ , a function $A (f)_{i} : A (y)_{i} \to A (x)_{Γ (f) (i)}$ .

This data is subject to a functoriality requirement: $A (g \circ f)_{i} = A (g)_{Γ (f) (i)} \circ A (f)_{i}$ and $A (id)_{i} = id$ .

Alternatively, $A$ can be viewed as a presheaf on the category of elements of $Γ$ .

A term $t$ of type $A$ in context $Γ$ consists of, for each object $x \in C$ and for each element $i \in Γ (x)$ , an element $t (x)_{i} \in A (x)_{i}$ , such that these choices are natural: for $f : x \to y$ in $C$ and $i \in Γ (y)$ , we should have $A (f)_{i} (t (y)_{i}) = t (x)_{Γ (f) (i)}$ .

For a natural transformation $σ : Δ \to Γ$ , the substituted type $A [σ]$ is defined by precomposition: it maps an object $x \in C$ and an element $i \in Δ (x)$ to the set $A (x)_{σ (x) (i)}$ , and it maps a morphism $f : x \to y$ in $C$ and an element $i \in Δ (y)$ to the function $A (f)_{σ (y) (i)}$ . Term substitution is also defined by precomposition: $t [σ]$ maps an object $x \in C$ and an element $i \in Δ (x)$ to the element $t (x)_{σ (x) (i)} \in A (x)_{σ (x) (i)}$ .

The empty context is the presheaf mapping every object to a fixed singleton set. The extended context $Γ ▹ A$ maps an object $x \in C$ to the set of pairs of an element $i \in Γ (x)$ and an element of $A (x)_{i}$ , and a morphism $f : x \to y$ in $C$ to the function $(i, a) \mapsto (Γ (f) (i), A (f)_{i} (a))$ . The extended substitution $σ ▹ t$ maps an object $x \in C$ to the function $i \mapsto (σ (x) (i), t (x)_{i})$ .

Other models

Other models of type theory include the setoid model, the groupoid model, the simplicial set model, the assemblies model, and several models in cubical sets starting with the BCH (Bezem–Coquand–Huber) model.

Relationship to categorical logic

Traditional categorical logic involves correspondences between logics and kinds of categories which serve as their models. For example, elementary toposes are models of a form of intuitionistic higher-order logic, and regular categories are models of regular logic. The correspondence is used in both ways: a notion of model is fundamental to study a logic, e.g., to prove that a statement is unprovable by finding a model where it fails, and conversely, a category can be studied by reasoning in a logic of which it is a model, which is often called an internal language for the category.

For simple type theory, such correspondences can be found. For example, Cartesian closed categories model the simply typed λ-calculus with function, top and product types, and bicartesian closed categories model its extension with bottom and sum types. On the other hand, the situation is significantly more complicated for dependent type theory.

In the aforementioned semantics of simple type theory, a type is interpreted by an object of the category. In dependent type theory, a type depends on the value of the context in which it is defined, so one cannot simply use an object. Instead, a natural idea is to interpret a type $A$ in context $Γ$ by an object equipped with a morphism to the interpretation of $Γ$ . The idea is to mimic the category of sets, where a family of sets $(A_{i})_{i \in Γ}$ can be represented categorically as the morphism $r : A \to Γ$ , where $A$ is the disjoint union of all the $A_{i}$ , which sends elements of each $A_{i}$ to their index $i$ . The family $(A_{i})$ can be recovered by $A_{i} = r^{- 1} (i)$ .

This idea was used by Seely in a 1984 paper claiming that Martin–Löf type theory with Π types, Σ types and extensional identity types can be modelled in a locally Cartesian closed category (i.e., a category $C$ such that all the slice categories $C / A$ are Cartesian closed). However, it was later observed that Seely's proof is wrong. Substitution in types is modelled by pullback. For the interpretation of substitution to be sound, this operation must be strictly functorial way: pullback along $g \circ f$ must be exactly the same as pullback along $f$ followed by pullback along $g$ . However, pullback involves an arbitrary choice and there is no reason for all these choices to be globally coherent: these pullbacks are always isomorphic, but have no reason to be the same. (Taking a skeleton of $C$ does not help, since a pullback is not merely a choice of object but also a choice of morphisms.)

For example, call $S : N \to N$ the successor constructor of natural numbers, and consider the trivial proof that for a predicate $P : N \to U$ , if $P (0)$ holds, $P (1)$ holds, and $P (n)$ holds for all $n \geq 2$ (call this hypothesis $H$ ), then $P (n)$ for all $n$ . This is done by two inductions: the first reduces to proving $(P (n)) [n := S (n^{'})]$ where $n^{'} : N$ is a fresh variable, and the second reduces this to proving $((P (n) [n := S (n^{'})]) [n^{'} := S (n^{″})]$ where $n^{″} : N$ is fresh. By applying the hypothesis $H$ to $S (S (n^{″}))$ (noting that $S (S (n^{″})) \geq 2$ ), one obtains an element of $(P (n)) [n := S (S (n^{″}))]$ . This only works because in the syntax of type theory, the substituted types $(P (n)) [n := S (S (n^{″}))]$ and $((P (n)) [n := S (n^{'})]) [n^{'} := S (n^{″})]$ are the same, namely $P (S (S (n^{″}))$ . On the other hand, using the interpretation of substitution as pullback, the interpretations of these two types would only be isomorphic and it would not be semantically justified to use elements of one as elements of the other.

The same problem arises with the interpretation of type formers, which must commute with substitution, whereas this fails in Seely's purported model. For example, given a dependent function $f : (x : A) \to (P (x) \times Q (x))$ , the application $f (g (y))$ has type $(P (x) \times Q (x)) [x := g (y)]$ . Without an actual equality between this type and $P (g (y)) \times Q (g (y))$ , it is not semantically justified to apply the first projection to $f (g (y))$ to obtain an element of $P (g (y))$ .

For this reason, type theory is not modelled directly in categories with properties, but rather in categories enriched with structure, such as CwFs, which include a set of types for each context and a substitution operation on types required to be functorial. The usual way to define a model is to start from a category with good enough properties and define this structure analogously to categorical constructions, but taking care to preserve coherence. This process is sometimes referred to as strictification.

There are several strictification constructions for doing this in general. A construction due to Bénabou was used by Hofmann to interpret MLTT in any locally Cartesian closed category, thus repairing Seely's result (with a different semantic interpretation). More recently, Lumsdaine and Warren proposed the local universes construction, which delays computing pullbacks by modelling a type in $Γ$ as two objects $U$ and $A$ with a pair of morphisms $Γ \to U \leftarrow A$ , so that applying a substitution $Δ \to Γ$ can be simply performed by composition of $Δ \to Γ$ with $Γ \to U$ , which is functorial.

However, in most concrete cases, the strictification can be done by hand, and the result is simpler to work with than the output of such general constructions. For example, in the set model, types in context $Γ$ are defined as the actual families of sets $(A_{i})_{i \in Γ}$ rather than a functions $A \to Γ$ so that the application of a substitution $γ : Δ \to Γ$ can simply be the family $(A_{γ (j)})_{j \in J}$ . This definition of substitution is strictly functorial, unlike pullback in the category of sets. The presheaf model is another typical example: substitution is made functorial by replacing presheaves $A$ with a natural transformation to $Γ$ by dependent presheaves over $Γ$ .