Semantics of type theory

The semantics of type theory involves several closely related kinds 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.

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 of a set of contexts denoted . To each derivable judgment “ is a type in context ” is associated an element of a set of types in context denoted . (Here depends on and not merely on although this dependency is dropped in the notation.) To each derivable judgment “ is a term of type in context ” (usually denoted ) is associated an element of a set of terms of type in context , denoted .

(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 “ and are definitionally equal types in context ” is derivable, the interpretation in the model must ensure , and whenever “ and are definitionally equal terms of type in context ” is derivable, the interpretation ensures .

A CwF contains operations to interpret contexts: a special element 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 has the dependent function type where is a term involving the variable , the application of to a term has the type . 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 to 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 in the syntax would be a term of type in context and a term of type in context ).

Definition

Let denote the category of families of sets. An object of is a family where is a set and each is a set. A morphism in is a function together with, for each , a function . (This category is equivalent to the arrow category of , through the correspondence between a function and the family of sets .)

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

A category.The class of objects is denoted and the objects are called contexts. The class of morphisms from a context to a context is denoted and these morphisms are called substitutions from to . A contravariant functor from this category to .The image of a context is a family of sets denoted (we usually drop the subscript in ). The elements of are called types in context , and the elements of are called terms of type (in context ).The image of a substitution is a morphism in . Its component is denoted by , and for each , its component is also denoted . These operations are respectively called substitution in types and substitution in terms.Alternatively, this data can be packaged as a presheaf of types on the category of contexts, and a dependent presheaf of terms 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 , consider the presheaf on the category of contexts which sends a context to the set of pairs of a substitution and a term . The functorial action of the presheaf on a substitution is given by . 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 and called the context extension of by .In one direction, the natural isomorphism sends a substitution and a term to a new substitution called the substitution extension of by . In the other direction, it sends a substitution to a pair of its tail and its head term .Explicitly, the fact that this is a natural isomorphism means that the following laws hold:

Defined operations

Let be a context and a type in . The head and tail of the identity substitution from to itself are respectively a substitution called weakening, and a term 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 by

and

Furthermore, given a substitution , and a type , we define a lifted substitution by .

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., is . 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

The corresponding operation on a CwF is: for each , for each , and for each , a type . This operation is required to satisfy the substitution rule: for all substitution and types , we must have .

The term formation rules for the pairing operation is:

The corresponding operation on a CwF is: for each , , , and ), a term . This must satisfy the substitution rule:

This equation is meaningful because of the CwF laws and the substitution rule for . The left hand side is an element of , which by the substitution rule for is equal to . To see that the right hand side is in this set, one has to check that is in . This holds because is in and

while

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

and the uniqueness rule (or η-rule)

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

and (for , , , , ), (for , , , ).

Universes

The case of universes is somewhat special because it is common to define the syntax of type theory without a separate judgment for “ is a type in context ”, instead using “ is a term of type in context ”, i.e., , where is the -th universe (also denoted , 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 containing itself (the syntax has the type in type rule that has type , which is inconsistent). The corresponding requirements on a CwF are: For each context , a type (we leave the dependency on implicit to lighten the notation), with the substitution rule . (This is equivalent to the data of a single type in the empty context , the version in an arbitrary context being recovered as where is the unique substitution from to .) An equality of sets for every context .

For a hierarchy of universes , where has type , …, 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 , a functor from this category to families of sets, mapping a context to a family of types of level and terms of these types, equipped with an operation to extend the context with a type of level (giving for a bijection natural in ). One can then model universes with, for each level , types with the substitution rule , and an equality of sets .

A slightly weaker variant is Coquand universes, which require a bijection between the sets and natural in , instead of an equality. This corresponds to a syntax with a primitive operation that takes an element of the universe (a “code” for a type) and gives an actual type, and another primitive operation that converts back a type into a code, with definitional equalities and . 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 operation but not a operation, and which require, for each type former, a counterpart on the level of codes, e.g., an operation on with the definitional equality , 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 , 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 , which is essentially equivalent to an iterated Σ-type . 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 for some closed type (i.e., a type in the empty context ).

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 , and a term of this type is a choice of an element for each . The action of a substitution on a type gives , and on a term , it gives . The empty context is a fixed singleton set. The extension of a context by a type is the type of pairs of an and an element of . The tail and head of a substitution are given by and .

All type formers are defined “pointwise”. For example, the product is defined as , the pairing of terms and is , 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