Intuitionistic Type Theory: Encyclopedia II - Intuitionistic Type Theory - Categorical models of Type Theory

Intuitionistic Type Theory - Categorical models of Type Theory

Using the language of category theory, Seely introduced the notion of a locally cartesian closed category (LCCC) as the basic model of Type Theory. This has been refined by Hofmann and Dybjer to Categories with Families or Categories with Attributes based on earlier work by Cartmell.

A category with families is a category C of contexts (in which the objects are contexts, and the context morphisms are substitutions), together with a functor T : C^op -> Fam(Set). Fam(Set) is the category in which the objects are pairs (A,B) of a set A and a set-valued function B, and the morphisms are functions f : A -> A' between the index sets to gether with, for all indices a : A a function g : B -> (B'.f).

The functor T assigns to a context G a set Ty(G) of types, and for each A : Ty(G), a set Tm(G,A) of terms. The axioms for a functor require that these play harmoniously with substitution. Substitution is usually written in the form Af or af, where A is a type in Ty(G) and a is a term in Tm(G,A), and f is a substitution from D to G. Here Af : Ty(D) and af : Tm(D,Af).

The category C must contain a terminal object (the empty context), and a final object for a form of product called comprehension, or context extension, in which the right element is a type in the context of the left element. If G is a context, and A : Ty(G), then there should be an object (G,A) final among contexts D with mappings p : D -> G, q : Tm(D,Ap).

A logical framework, such as Martin-Löf's takes the form of closure conditions on the context dependent sets of types and terms: that there should be a type called Set, and for each set a type, that the types should be closed under forms of dependent sum and product, and so forth.

A theory such as that of predicative set theory expresses closure conditions on the types of sets and their elements: that they should be closed under operations that reflect dependent sum and product, and under various forms of inductive definition..

Adapted from the Wikipedia article "Categorical models of Type Theory", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki