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 denote the category of families of sets: an object is a family where each is a set, and a morphism is a function together with, for each, a function.A category with families consists of the following data:
- A category, whose class of objects is denoted and whose class of morphisms from to is denoted. The objects are called contexts and the morphisms are called substitutions.
- A contravariant functor from the category of contexts to. The image of a context is denoted. The elements of are called types in context, and the elements of are called terms of type . The image of a substitution is a morphism in. Its component is denoted by, and for each, its component is also denoted.
- A terminal object in the category of contexts, called the empty context and denoted.
- For each context and for each type, a representing object for the presheaf on the slice category that sends a substitution to the set , along with a natural isomorphism witnessing that this object represents the presheaf. This representing object consists of a context denoted, called the extension of by, along with a substitution called weakening. The natural isomorphism sends a substitution and a term to a substitution denoted, called the extension of by.