Syntax and Semantics of Dependent Types

Martin Hofmann

1 Introduction

Dependent types are types which unlike simple types, such as products, function spaces, or natural numbers, depend on or vary with values. An example of a dependent type is a type of vectors or arrays Vec_{σ}(M) of a given length M : N over some type σ. Its objects are nil_{σ} : Vec_{σ}(0) and Cons_{σ}(U, V) : Vec_{σ}(Suc(M)) where U : σ and V : Vec_{σ}(M). We can now consider a function which given x: N returns a vector (over N) of length x and all entries 0. This function then has the type Πx: N.Vec_{N}(x) — a type of functions with the property that the type of the result depends on the argument. The same algorithm could also be typed as N → List(N). The point of the dependent typing is that it reveals more information about the function. Another example of this kind is the exception-free head function for vectors

Hd : Πx: N.Vec_{σ}(Suc(x)) → σ

which yields the first entry of a vector. The typing prevents the unwanted case that Hd gets applied to the empty list. In this way the dependent typing circumvents the need for partial functions in certain cases.

Another source for type dependency comes from type variables and type universes. For instance, the type of monoids with carrier X

MON (X) =^{def} ((X × X) → X) × X

is a type depending on X. Type variables such as X above can be treated as ordinary variables using universes, that is types containing (names for) other types as members. The function constructing the free monoid on a type X would then be given the type

ΠX: U .MON (List(X))

where U is such a universe.

The third important source for dependent types comes from the propositionsas-types analogy under which propositions (in constructive logic) are seen as types, namely the type of their proofs. For instance, a proof of ϕ ∧ ψ consists of a proof of ϕ and a proof of ψ; a proof of ϕ ⊃ ψ consists of a procedure which transforms a hypothetical proof of ϕ into a proof of ψ. Therefore, conjunction and implication can be identified with cartesian product and function space, respectively. Under this correspondence, predicates, i.e. propositional functions become dependent types. We will describe how to view the atomic equality predicate and universal and existential quantification as types and type formers. In fact universal quantification corresponds to the Π-type introduced above.

If propositions are ordinary types they can be part of other types. For instance, we can enrich the above-defined type of monoids of monoids by a proposition stating associativity and neutrality:

MON′(X) =^{def}

Σ∘ : (X × X) → X. Σe : X. (∀x, y, z: X. ∘ (∘(x, y), z) = ∘(x, ∘(y, z))) ∧ (∀x: X. ∘ (e, x) = x ∧ ∘(x, e) = e)

The Σ-type former is a generalisation of the cartesian product × to dependent types and corresponds under the propositions-as-types analogy to existential quantification. An object of the above generalised signature thus consists of

• an object ∘ of type (X × X) → X

• an object e of type X

• a proof that ∘ is associative and e is neutral

The main aim of this article is not so much to explain how to use dependent types to formalise constructive mathematics or to do program development and specification, but rather to introduce the reader to a tool for the metatheoretic study of dependent type theory: category-theoretic semantics.

By semantics we understand a compositional assignment of mathematical objects to syntactic objects, for instance sets or sets to types and set-theoretic functions to (open) terms of the types. Such interpretation is performed with the aim of establishing consistency or conservativity of certain type-theoretic constructs, or simply in order to explain, motivate, and justify them. Due to type dependency the verification that such an interpretation indeed validates all the rules of type theory can be quite involved which is why it has proven useful to define a general abstract notion: the category-theoretic semantics, which is proven sound and complete once and for all. Then in order to obtain an interpretation of type theory one “only” needs to check that one has an instance of the semantic notion.

The semantics is not surprising (like maybe the set-theoretic semantics for first-order logic) in that we have an almost trivial completeness property like in the case of Heyting algebra semantics for intuitionistic logic. The point is that the soundness theorem is non-trivial and therefore some work can be saved when presenting a translation of the syntax as a model construction.

1.1 Overview

In the next section we give the syntax for an extensible calculus of dependent types which encompasses various “named” type theories like Martin-Löf’s type theory or the Calculus of Constructions. In §§2.4 & 2.3 we introduce pre-syntax and syntactic context morphisms. Both are auxiliary syntactic notions required later to define the interpretation function and to construct a term model. §3 contains the material on category-theoretic semantics. It introduces categories with families which provide a category-theoretic counterpart of type dependency and form the backbone of the semantics. We compare this notion to related concepts and identify the additional structure required to model the type and term formers. Section 3 ends with the interpretation of the syntax in the semantic structures. Finally, §4 is devoted to an extended application of the material: we give an interpretation of types as “variable sets” (presheaves) and use it to establish conservativity of Martin-Löf’s Logical Framework over ordinary type theory.

Every section or larger subsection except the last one ends with several exercises which either contain definitions or proofs which are similar to previously given ones and are required later, or contain applications of the material. The last section contains instead an overview of the literature on applications of semantic methods to dependent type theory as a suggestion for further reading.

This article is self-contained except for the presupposition of some very basic category theory in §§3 & 4 which have not been included as very good introductions are readily available. The required notions are summarised in the beginning of §3.

2 Formal systems for dependent types

A theory of dependent types is a formal system which mainly allows one to derive judgements of the form M : σ (the term M has type σ) and σ type (σ is a type). As types may contain terms, typing affects typehood and both kinds of judgements must be defined simultaneously. For instance, Vec_{σ}(M) is a type if σ is a type and M : N. Furthermore, we usually want a notion of definitional equality to be built into the theory, for example we wish to consider 0 : N and 0 + 0 : N as (definitionally) equal terms and hence Vec_{σ}(0) and Vec_{σ}(0 + 0) as definitionally equal types: if M : Vec_{σ}(0) then also M : Vec_{σ}(0+0). This leads to two more forms of judgement: M = N : σ (M and N are definitionally equal terms of type σ) and σ = τ type (σ and τ are definitionally equal types). Finally, we must keep track of the types of the free variables occurring in a judgement; we cannot assert x + y : N unless we know that x: N and y: N. Since such declarations may depend on each other like in x: N, y: Vec_{N}(x) it is convenient to make all judgements relative to a list of variable declarations including at least the free variables occurring inside the judgement. Such lists of declarations are called contexts and sometimes also type assignments. Intuitively, a context x_{1}: σ_{1}, …, x_{n}: σ_{n} is well-formed if each σ_{i} is a type in the context x_{1}: σ_{1}, … x_{i−1}: σ_{i−1} and the x_{i} are pair-wise distinct. So typehood (and thus typing) affects context validity and we finally arrive at six kinds of judgements:

⊢ Γ ctxt Γ is a valid context Γ ⊢ σ type σ is a type in context Γ Γ ⊢ M : σ M is a term of type σ in context Γ ⊢ Γ = Δ ctxt Γ and Δ are definitionally equal contexts Γ ⊢ σ = τ type σ and τ are definitionally equal types in context Γ Γ ⊢ M = N : σ M and N are def. equal terms of type σ in context Γ.

Well-formedness and equality of contexts can be defined in terms of the other judgements, but it is technically easier to include them as primary notions.

Regardless of which rules we later introduce to describe particular type and term formers such as the natural numbers or Π-types we always have the following structural rules.

• Rules for context formation:

\overline{⊢ ⋄ ctxt} C-Emp  \frac{Γ ⊢ σ type}{⊢ Γ, x: σ ctxt} C-Ext

\frac{⊢ Γ = Δ ctxt Γ ⊢ σ = τ type}{⊢ Γ, x: σ = Δ, y: τ ctxt} C-Ext-Eq

The variables x and y in rules C-Ext and C-Ext-Eq are assumed to be fresh.

• The variable rule

\frac{⊢ Γ, x: σ, Δ ctxt}{Γ, x: σ, Δ ⊢ x : σ} Var

• Rules expressing that definitional equality is an equivalence relation:

\frac{⊢ Γ ctxt}{⊢ Γ = Γ ctxt} C-Eq-R

\frac{⊢ Γ = Δ ctxt}{⊢ Δ = Γ ctxt} C-Eq-S

\frac{⊢ Γ = Δ ctxt  ⊢ Δ = Θ ctxt}{⊢ Γ = Θ ctxt} C-Eq-T

\frac{Γ ⊢ σ type}{Γ ⊢ σ = σ type} Ty-Eq-R

\frac{Γ ⊢ σ = τ type}{Γ ⊢ τ = σ type} Ty-Eq-S

\frac{Γ ⊢ σ = τ type Γ ⊢ τ = ρ type}{Γ ⊢ σ = ρ type} Ty-Eq-T

\frac{Γ ⊢ M : σ}{Γ ⊢ M = M : σ} Tm-Eq-R

\frac{Γ ⊢ M = N : σ}{Γ ⊢ N = M : σ} Tm-Eq-S

\frac{Γ ⊢ M = N : σ Γ ⊢ N = O : σ}{Γ ⊢ M = O : σ} Tm-Eq-T

• Rules relating typing and definitional equality:

\frac{Γ ⊢ M : σ  ⊢ Γ = Δ ctxt Γ ⊢ σ = τ type}{Δ ⊢ M : τ} Tm-Conv

\frac{⊢ Γ = Δ ctxt Γ ⊢ σ type}{Δ ⊢ σ type} Ty-Conv

• For convenience (cf. E2.7 below) we also introduce the following weakening and substitution rules where J ranges over one of the judgements M : σ, σ type, M = N : σ, σ = τ type.

\frac{Γ, Δ ⊢ J  Γ ⊢ ρ type}{Γ, x: ρ, Δ ⊢ J} Weak

\frac{Γ, x: ρ, Δ ⊢ J  Γ ⊢ U : ρ}{Γ, Δ[U/x] ⊢ J [U/x]} Subst

Here J [U/x] (and similarly Δ[U/x]) denotes the capture-free substitution of U for x in J. This means that bound variables in J are systematically renamed so as to prevent any free variables in U from becoming bound in J [U/x]. We will henceforth consider all contexts, types, and terms as equal if they agree up to names of bound variables and assume the existence of a capture-free substitution function on these equivalence classes. One can use a de Bruijn style presentation of the syntax to avoid this identification. A good reference is (Huet 1990). The de Bruijn presentation gives rise to canonical representatives of the equivalence classes and yields an algorithm implementing capture-free substitution.

2.1 Type formers

Type and term formers are introduced by formation, introduction, elimination, and equality rules. There is no definitive set of type formers and new ones can be invented as needed. We present several of them to give an idea of the general pattern.

2.1.1 Dependent function space

The dependent function space also called dependent product or Π-type corresponds to the set-theoretic notion of cartesian product over a family of sets Π_{i∈I}B_{i} which has as elements functions mapping an index i to an element of the corresponding set B_{i}. In type theory this is expressed as follows:

\frac{Γ ⊢ σ type Γ, x: σ ⊢ τ type}{Γ ⊢ Πx: σ.τ type} Π-F

\frac{Γ ⊢ σ_{1} = σ_{2} type Γ, x: σ ⊢ τ_{1} = τ_{2} type}{Γ ⊢ Πx: σ_{1}.τ_{1} = Πx: σ_{2}.τ_{2} type} Π-Eq

The first rule expresses that a dependent function space consists of a type σ (possibly depending on other types recorded in Γ) and a type depending on σ (and Γ), viz. τ. The rule Π-Eq expresses that definitional equality is respected by the Π-former. The variable x becomes bound in Πx: σ.τ and thus this type is subject to the convention on renaming of variables set out above. To form elements of the Π-type we have the introduction rule with associated congruence rule:

\frac{Γ, x: σ ⊢ M : τ}{Γ ⊢ λx: σ.M^{τ} : Πx: σ.τ} Π-I

\frac{Γ, x: σ ⊢ M_{1} = M_{2} : τ Γ ⊢ σ_{1} = σ_{2} type Γ, x: σ ⊢ τ_{1} = τ_{2} type}{Γ ⊢ λx: σ_{1}.M_{1}^{τ_{1}} = λx: σ_{2}.M_{2}^{τ_{2}} : Πx: σ_{1}.τ_{1}} Π-I-Eq

So to give an element of Πx: σ.τ one must give an element of τ[x] in the presence of a variable x of type σ. The congruence rule Π-I-Eq expresses that definitional equality preserves Π-introduction (λ). We will henceforth refrain from writing down congruence rules. Such rules are silently understood for every type and term former we will introduce.

Elements of a Π-type are consumed using application like in the settheoretic situation where an element of Π_{i∈I}B_{i} and a specific i_{0} ∈ I gives an element of B_{i_{0}}:

\frac{Γ ⊢ M : Πx: σ.τ Γ ⊢ N : σ}{Γ ⊢ App_{[x:σ]τ}(M, N) : τ[N/x]} Π-E

Notice that the square brackets in the typing annotation [x: σ]τ are an integral part of the term former for application and indicate the binding of x in τ. Now we encounter a source for definitional equality: applying a function λx: σ.M^{τ} to a term N : σ results in M with x replaced by N:

\frac{Γ ⊢ λx: σ.M^{τ} : Πx: σ.τ Γ ⊢ N : σ}{Γ ⊢ App_{[x:σ]τ}(λx: σ.M^{τ}, N) = M[N/x] : τ[N/x]} Π-C

Notice that substitution plays a more prominent role in dependently typed calculi as it is needed to formulate even the typing rules, not only the conversion rules (as in the case of simply-typed lambda calculus).

The attribute “definitional” for en equation like Π-C is certainly arguable. It is motivated by the understanding of λx: σ.M^{τ} as a canonical element of Πx: σ.τ and application as a derived concept defined by equation Π-C. This view becomes important if one wants to see type theory as a foundation of constructive mathematics which accordingly is to be justified by a philosophical argument rather than via an interpretation in some other system, see (Martin-Löf 1975;(1984)). For us the distinction between canonical and noncanonical elements is not important. However, we will use it to motivate further definitional equalities.

A more pragmatic explanation for Π-C is that in applications one often uses abstraction as a means for making definitions and application to instantiate a definition. Thus when the Π-type is used in this way then both sides of Π-C are indeed definitionally equal in the proper sense of the word.

2.1.2 Dependent sum

The next type former we introduce is the Σ-type (or dependent sum) corresponding to disjoint union in set theory. If we are given a family of sets (B_{i})_{i∈I} we can form the set Σ_{i∈I}B_{i} =^{def} {(i, b) | i ∈ I ∧ b ∈ B_{i}} whose elements consist of an index i and an element of the corresponding set B_{i}. In type theory the corresponding formation and introduction rules look as follows.

\frac{Γ ⊢ σ type Γ, x: σ ⊢ τ type}{Γ ⊢ Σx: σ.τ type} Σ-F  \frac{\begin{matrix}Γ ⊢ M : σ \\ Γ ⊢ N : τ[M/x] \end{matrix}}{Γ ⊢ Pair_{[x:σ]τ}(M, N) : Σx: σ.τ} Σ-I

The elimination rule looks a bit complicated at first sight:

\frac{Γ, z: Σx: σ.τ ⊢ ρ type Γ, x: σ, y: τ ⊢ H : ρ[Pair_{x:σ.τ}(x, y)/z] Γ ⊢ M : Σx: σ.τ}{Γ ⊢ R_{[z:Σx:σ.τ]ρ}^{Σ}([x: σ.y: τ]H, M) : ρ[M/z]} Σ-E

Here the variable z in ρ and the variables x, y in H become bound inside R^{Σ} as indicated by the square brackets. The idea behind R^{Σ} is that in order to give a (possibly dependent) function out of Σx: σ.τ, it is enough to specify it on canonical elements, viz. the pairs. This is expressed by the following definitional equality

\frac{Γ ⊢ R_{[z:Σx:σ.τ]ρ}^{Σ}([x: σ, y: τ]H, Pair_{[x:σ]τ}(M, N)) : ρ[Pair_{[x:σ]τ}/z]}{Γ ⊢ R_{[z:Σx:σ.τ]ρ}^{Σ}([x: σ, y: τ]H, Pair_{[x:σ]τ}(M, N)) = H[M/x, N/y] : ρ[Pair_{[x:σ]τ}/z]} Σ-C

which says that a function on Σx: σ.τ defined using the eliminator R^{Σ} behaves on canonical elements as specified by the argument H. As an example we show how to define projections for the Σ-type. Assume Γ ⊢ σ type, Γ, x: σ ⊢ τ type, and Γ ⊢ M : Σx: σ.τ. We define

M.1 =^{def} R_{[z:Σx:σ.τ]σ}^{Σ}([x: σ, y: τ]x, M) : σ

Now, in the particular case where M is canonical, i.e. M ≡ Pair_{[x:σ]τ}(U, V) the rule Σ-C gives Γ ⊢ M.1 = U : σ as expected. A second projection can be defined similarly:

M.2 =^{def} R_{[z:Σx:σ.τ]τ[z.1/x]}^{Σ}([x: σ, y: τ]y, M) : τ[M.1]

Notice that the definiens (the right-hand side) is well-typed by virtue of rules Σ-C and Ty-Conv which allow us to conclude

Γ, x: σ, y: τ ⊢ y : τ[(Pair_{[x:σ]τ}(x, y).1)/x]

One can restrict the elimination operator R^{Σ} to those cases where the type ρ does not depend on Σx: σ.τ. One can then still define the first projection, but no longer the second one. This is called weak Σ-elimination, see (Luo 1994).

Important special cases of Πx: σ.τ and Σx: σ.τ arise when τ does not actually depend on σ. In this case, i.e. when Γ ⊢ σ type and Γ ⊢ τ type we write

σ → τ =^{def} Πx: σ.τ

and

σ × τ =^{def} Σx: σ.τ

indicating that in these cases the Π- and Σ-types correspond to ordinary non-dependent function space and cartesian product, respectively.

A (constructive) proof of an existential statement ∃x: σ.P (x) consists of an element M of σ (the witness) together with a proof that P (M), that is an element of P (M). Thus under the propositions-as-types analogy the Σ-type is the counterpart to existential quantification.

2.1.3 Natural numbers

An example of a basic type is provided by the type of natural numbers given by the rules

\frac{⊢ Γ ctxt}{Γ ⊢ N type} N-F  \frac{⊢ Γ ctxt}{Γ ⊢ 0 : N} N-I-0  \frac{Γ ⊢ M : N}{Γ ⊢ Suc(M) : N} N-I-S

The elimination rule is similar to the one for Σ-types; in order to define a (possibly dependent) function on N it is enough to give it on the canonical elements 0 and Suc(M). In the case of Suc(M) the function may be called (primitive) recursively for M.

\frac{Γ, n: N ⊢ σ type Γ ⊢ H_{z} : σ[0/n] Γ, n: N, x: σ ⊢ H_{s} : σ[Suc(n)/n] Γ ⊢ M : N}{Γ ⊢ R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, M) : σ[M/n]} N-E

The primitive-recursive behaviour of R^{N} is expressed by the following two rules for definitional equality:

\frac{Γ ⊢ R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, 0) : σ[0/n]}{Γ ⊢ R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, 0) = H_{z} : σ[0/n]} N-C-0

\frac{Γ ⊢ R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, Suc(M)) : σ[Suc(M)/n] N-C-S}{Γ ⊢ R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, Suc(M)) = H_{s}[M/n, R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, M)/x] : σ[Suc(M)/n]}

The elimination rule for natural numbers allows for both the definition of functions by primitive recursion and proof of properties of the natural numbers by mathematical induction. For instance, we can define addition as follows

M + N =^{def} R_{[n:N]N}^{N}(N, [n: N, x: N]Suc(x), M) : N

and—writing n̄ for the closed term \underbrace{Suc(… Suc(}_{n times} 0) …)—we have

⋄ ⊢ n̄ + m̄ = \overline{m + n} : N

for all (set-theoretic) natural numbers m, n by m-fold application of rule N-C-S followed by N-C-Z. We will see an example of the use of mathematical induction below.

2.1.4 Notation

We will henceforth freely suppress type annotations if this increases readability. For instance, we may write λx: σ.M or even λx.M instead of λx: σ.M^{τ}. We sometimes omit a prevailing context Γ and thus write ⊢ J instead of Γ ⊢ J. We write ⋄ ⊢ J if we want to emphasise that a judgement holds in the empty context. If σ contains among others the free variable x then we can write σ[x] to emphasise this and use the notation σ[M] for σ[M/x] in this case.

In implementations of type theory many more such conventions are being used and sometimes they are even made part of the official syntax. It is always an important question whether such shorthands should be treated formally or informally. Here we have decided to have a syntax as explicit as possible so as to facilitate its meta-theoretic study. For doing proofs within the theory obviously the syntactic sugar is unavoidable.

2.1.5 Identity types

As we have explained, definitional equality is the congruence generated by the computational equations like N-C-Z and Π-C. Its main purpose is to facilitate the construction of inhabitants of types; in some examples, like the definition of the second projection for Σ-types above, its use is unavoidable. However, definitional equality is merely a judgement, and not a type, that is, not a proposition, and therefore cannot be established by induction, i.e., using R^{N} or R^{Σ}. Also, we cannot have definitional equalities as assumptions in a context. In order to enable equality reasoning inside type theory one is therefore lead to introduce a type corresponding to equality—the identity type. For every two terms of the same type we have a (not necessarily inhabited) type of proofs of their equality

\frac{Γ ⊢ M : σ Γ ⊢ N : σ}{Γ ⊢ Id_{σ}(M, N) type} Id-F

and the identity types have canonical inhabitants corresponding to reflexivity

\frac{Γ ⊢ M : σ}{Γ ⊢ Refl_{σ}(M) : Id_{σ}(M, M)} Id-I

We call two terms Γ ⊢ M, N : σ propositionally equal if the type Γ ⊢ Id_{σ}(M, N) is inhabited. By the (implicit) congruence rules and rule Ty-Conv propositional equality extends definitional equality, that is, we have Γ ⊢ Refl_{σ}(M) : Id_{σ}(M, N) provided Γ ⊢ M = N : σ.

So far we only know that propositional equality is a reflexive relation. The further properties like symmetry, transitivity, Leibniz’ principle are all consequences of the following elimination rule for identity types

\frac{Γ ⊢ σ type Γ , x: σ, y: σ , p: Id_{σ}(x, y) ⊢ τ type Γ, z: σ ⊢ H : τ[z/x, z/y, Refl_{σ}(z)/p] Γ ⊢ M: σ Γ ⊢ N: σ Γ ⊢ P : Id_{σ}(M, N)}{Γ ⊢ R_{[x:σ,y:σ,p:Id_{σ}(x,y)]τ}^{Id}([z: σ]H , M, N, P) : τ[M/x, N/y, P/p]} Id-E

and the associated equality rule

\frac{Γ ⊢ R_{[x:σ,y:σ,p:Id_{σ}(x,y)]τ}^{Id}([z: σ]H , M, M, Refl_{σ}(M)) : τ[M/x, M/y, Refl_{σ}(M)/p]}{Γ ⊢ R_{[x:σ,y:σ,p:Id_{σ}(x,y)]τ}^{Id}([z: σ]H , M, M, Refl_{σ}(M)) = H[M/z] : τ[M/x, M/y, Refl_{σ}(M)/p] Id-C}

The eliminator R^{Id} is an induction principle like R^{N} and R^{Σ} which roughly states that every element of an indentity type behaves as if it were a canonical one of the form Refl_{σ}(M). We demonstrate how to derive Leibniz’ principle from R^{Id}: Suppose that x: σ ⊢ ρ[x] type, and that we are given two propositionally equal terms of type σ, i.e., ⊢ M, N : σ and ⊢ P : Id_{σ}(M, N). If ⊢ H : ρ[M] then we can construct an element Subst_{[x:σ]ρ}(P, H) of ρ[N] as follows. We define

τ[x: σ, y: σ, p: Id_{σ}(x, y)] =^{def} ρ[x] ⇒ ρ[y]

(Recall that ϕ ⇒ ψ abbreviates Πx: ϕ.ψ.) Now λh: ρ[x].h is an inhabitant of x: σ ⊢ τ[x, x, Refl_{σ}(x)], so

Subst_{[x:σ]ρ}(P, H) =^{def} App(R_{[x:σ,y:σ,p:Id(x,y)]}^{Id}([x: σ]λh: ρ[x].h , M, N, P) , H) : ρ[N]

and from Id-C and Π-C we get the derived rule Subst_{[x:σ]ρ}(Refl_{σ}(M), H) = H : ρ[M].

From Subst we can derive symmetry, transitivity, and congruence properties of propositional equality in the usual way. For example, if x: σ ⊢ U[x] : τ and ⊢ P : Id_{σ}(M, N) then

Resp_{σ,τ}([x: σ]U , P) =^{def}

Subst_{[x:σ]Id_{τ} (U[M],U[x])}(P, Refl_{τ}(U[M])) : Id_{τ}(U[M], U[N])

We can derive a similar congruence property in the case that τ depends on x; for this and other derived properties and combinators for propositional equality we refer to (Nordström, Petersson, and Smith 1990; Streicher 1993; Hofmann 1995a).

We have now collected enough material to carry out the promised example of a proof by induction. We wish to construct an element of the type

m: N ⊢ Id_{N}(m + 0, m) type

where + is the addition operation defined above. Notice that we have n: N ⊢ Refl_{N}(n) : Id_{N}(0 + n, n) immediately by N-E-Z and the definition of +. Let us define σ[m: N] =^{def} Id_{N}(m + 0, m). So σ is now a type with a distinguished free variable m. By N-C-Z we have

⊢ Refl_{N}(0) : σ[0]

Now by N-E-S we have

m: N ⊢ σ[Suc(m)] = Id_{N}(Suc(m), Suc(m + 0)) type

Therefore,

m: N, h: σ[m] ⊢ Resp_{N,N}([x: N]Suc(x) , h) : σ[Suc(m)]

and we can finally conclude

m: N ⊢ R_{[m:N]σ}^{N}( \begin{matrix}[t]Refl_{N}(0), \\ [m: N, h: σ]Resp_{N,N}([x: N]Suc(x) , h), \\ m) : σ[m] \end{matrix}

Again, we refer to (Nordström, Petersson, and Smith 1990) for more examples of this kind. The metatheory and the strength of the present and other formulations of the identity type have been analysed in (Hofmann 1995a;(1996);Streicher 1993).

We remark that propositional equality does not affect the definitional one which even in the presence of identity types remains confined to intensional equality. Therefore, type theory together with identity types as defined here is called intensional type theory, see (Martin-Löf 1982). There exists another formulation of identity types in which one may conclude Γ ⊢ M = N : σ from Γ ⊢ P : Id_{σ}(M, N). This rule is called equality reflection and makes it possible to derive “definitional” equalities by induction and thus makes it extensional. Therefore, type theory with equality reflection is called extensional type theory. Since the proof P is discarded upon application of this rule, definitional equality (then rather called judgemental equality) and thus typing become undecidable. See also E3.30.

2.1.6 Universes

A universe is a type containing codes for types. This is expressed by the following two rules

\frac{⊢ Γ ctxt}{Γ ⊢ U type} U-F  \frac{Γ ⊢ M : U}{Γ ⊢ El(M) type} El-F

So if M : U is such a “code” then we can form the type associated to M, namely El(M). So far the universe does not contain any closed codes. This may be achieved by stipulating that the universe be closed under certain type formers. For instance, closure under Π-types is expressed by

\frac{Γ ⊢ S : U  Γ, s: El(S) ⊢ T : U}{Γ ⊢ Π̂(S, [s: El(S)]T) : U} U-Π

\frac{Γ, s: El(S) ⊢ M : El(T)}{Γ ⊢ λ̂s: El(S).M^{El(T)} : El(Π̂(S, [s: El(S)]T))} U-Π-I

\frac{Γ ⊢ M : El(Π̂(S, [s: El(S)]T)) Γ ⊢ N : El(S)}{Γ ⊢ Âpp_{[s:El(S)]El(T)}(M, N) : El(T [N/s])} U-Π-E

\frac{Γ ⊢ Âpp_{[s:El(S)]El(T)}(λ̂s: El(S).M^{El(T)}, N) : El(T [N/s])}{Γ ⊢ Âpp_{[s:El(S)]El(T)}(λ̂s: El(S).M^{El(T)}, N) = M[N/s] : El(T [N/s])} U-Π-C

A more economic syntax for universes closed under Π-types is obtained if we replace the last three above rules by a single new type equality

\frac{Γ ⊢ Π̂(S, [s: El(S)]T) : U}{Γ ⊢ El(Π̂(S, [s: El(S)]T)) = Πs: El(S).El(T) type} U-Π-Ty

which states that El(Π̂(S, [s: El(S)]T)) is the product of the El(T) rather than behaving like it. One does not need the new application and abstraction operators λ̂ and Âpp then. This syntax, which in fact is often used in the literature, has the disadvantage that it is no longer the case that equal types share the same outermost type former. This makes it more difficult to show that the type formers are injective; an auxiliary property required to establish the subject reduction property for an untyped rewrite system derived from definitional equality. Also, in many models rule U-Π-Ty is not valid under the canonical interpretation of Π, see (Streicher 1991) and the example following Def. 3.20.

Closure under natural numbers is described by

\frac{⊢ Γ ctxt}{Γ ⊢ N̂ : U} U-N

and further rules introducing term formers ˆ0, Ŝuc, and R̂^{N} witnessing that El(N̂) behaves like N. Again we could instead impose the equality Γ ⊢ El(N̂) = N type if the type theory already contains natural numbers.

In a similar way closure under other type formers including another universe can be stipulated. A final important closure property for universes is impredicative quantification:

\frac{Γ ⊢ σ type Γ, x: σ ⊢ T : U}{Γ ⊢ ∀x: σ.T : U} U-∀

\frac{Γ, x: σ ⊢ M : El(T)}{Γ ⊢ λ̂x: σ.M^{El(T)} : El(∀x: σ.T)} U-∀-I

\frac{Γ ⊢ M : El(∀x: σ.T) Γ ⊢ N : σ}{Γ ⊢ Âpp_{[x:σ]El(T)}(M, N) : El(T [N/x])} U-∀-E

\frac{Γ ⊢ Âpp_{[x:σ]El(T)}λ̂x: σ.M^{El(T)}, N) : El(T [N/x])}{Γ ⊢ Âpp_{[x:σ]El(T)}(λ̂x: σ.M^{El(T)}, N) = M[N/x] : El(T [N/x])} U-∀-C

The difference to closure under Π-types is that the “domain-type” σ is arbitrary and not confined to a “small type” of the form El(S). In particular σ can be U itself and we can form terms like

polyone = ∀c: U .∀s: El(c).c

where El(polyone) has the closed inhabitant

⋄ ⊢ λ̂C: U .λ̂x: El(C).x : El(polyone)

—the polymorphic identity function known from polymorphic lambda calculus.

Universes are employed for modularisation and abstraction. For instance, they permit the definition of a type of a certain algebraic structure. In this way the type of semigroups with carrier X : U can be defined as

SEM (X) =^{def} Σ∘: El(X) × El(X) → El(X). Πx: El(X).Πy: El(X).Πz: El(X).Id_{El(X)}(∘(∘(x, y), z) , ∘(x, ∘(y, z)))

An element of type SEM (X) consists of a binary function on El(X), and a proof that this function is associative. We can now write a function F : ΠX: U .MON (X) → SEM (X) which “forgets” the neutral element. We can also form ΣX: U .SEM (X); the type of semigroups. More complex examples of this kind may be found in (Luo 1991). An application of this pattern to semantics of modules in functional languages is (Harper and Mitchell 1993).

Under the propositions-as-types analogy we can view a universe also as a type of propositions. For instance, the type σ → U can be viewed as an analogue to the power-set of σ.

2.1.7 Miscellaneous types

A counterpart to absurdity in logic is the following empty type:

\frac{⊢ Γ ctxt}{Γ ⊢ 0 type} 0-F  \frac{Γ ⊢ σ type Γ ⊢ M : 0}{Γ ⊢ R_{σ}^{0}(M) : σ} 0-E

There are no canonical elements in 0 so there is no “computation rule” like N-C-Z. It is sometimes useful to have a type with a single canonical element corresponding to the true proposition:

\frac{⊢ Γ ctxt}{Γ ⊢ 1 type} 1-F  \frac{⊢ Γ ctxt}{Γ ⊢ ⋆ : 1} 1-I

\frac{Γ, x: 1 ⊢ σ type Γ ⊢ H : σ[⋆/x] Γ ⊢ M : 1}{Γ ⊢ R_{[x:1]σ}^{1}(H, M) : σ[M/x]} 1-E

\frac{Γ ⊢ R_{[x:1]σ}^{1}(H, ⋆) : σ[⋆/x]}{Γ ⊢ R_{[x:1]σ}^{1}(H, M) = H : σ[M/x]} 1-C

There are a number of other types considered in the literature like co-product types corresponding to binary disjoint union, finite types with n elements for each natural number n, types of well-founded trees, subset types, and quotient types to name the most important ones. In implementations like Lego and Coq new type formers can be defined “on the fly” by giving the rules for their canonical elements (like Suc and 0 in the case of N). The elimination rules are then generated automatically. In Alf this is also possible, but elimination rules are replaced by the more general device of pattern-matching on the form of the constructors.

Finally, we can consider arbitrary theories of dependent types defined by type symbols, constants, and equations. This is described in (Pitts 1997).

2.2 Examples of type theories

In this section we briefly describe some “named” type theories and how they fit into the formal framework described here.

2.2.1 Martin-Löf’s type theory

This is a collective name for type theories containing several of the abovedescribed type formers, but not a universe closed under impredicative quantification. A characteristic feature of Martin-Löf’s type theory is the presence of identity types either with or without equality reflection. Martin-Löf invented his type theories with the aim of extending the propositions as types correspondence to predicate logic and to provide a universal language for constructive mathematics (Martin-Löf 1984; Martin-Löf 1975). A standard reference on Martin-Löf’s type theories is (Nordström, Petersson, and Smith 1990). An implementation of extensional Martin-Löf type theory is the Nuprl system (Constable et al. 1986).

2.2.2 The Logical Framework

Martin-Löf’s Logical Framework (LF), see Part IV of (Nordström, Petersson, and Smith 1990), is a type theory with Π-types and a universe. Its intended use is to define theories, in particular Martin-Löf type theory, as extensions of the LF by constants and equations.

The idea is that types and type formers are declared as constants in the universe and that term-formers are declared as constants of the appropriate El-types. To distinguish from object level type formers some different notation is used: the Π-type of the framework is written (x: σ)τ instead of Πx: σ.τ and (σ)τ instead of σ → τ. Iterated Π-types are written (x_{1}: σ_{1}, …, x_{n}: σ_{n})τ instead of Πx_{1}: σ_{1}…. Πx_{n}: σ_{n}.τ. Abstraction is written as [x: σ]M instead of λx: σ.M^{τ} and application is written M(N) instead of App_{[x:σ]τ}(M, N).^{1} Iterated abstractions and applications are written [x_{1}: σ_{1}, …, x_{n}: σ_{n}]M and M(N_{1}, …, N_{n}), respectively. The lacking type information can be inferred. The universe is written Set instead of U . The El-operator is omitted.

For example the Π-type is described by the following constant and equality declarations (understood in every valid context):

⊢ Π : (σ: Set, τ: (σ)Set)Set
⊢ App : (σ: Set, τ: (σ)Set, m: Π(σ, τ), n: σ)τ(m)
⊢ λ : (σ: Set, τ: (σ)Set, m: (x: σ)τ(x))Π(σ, τ)
σ: Set, τ: (σ)Set, m: (x: σ)τ(x), n: σ ⊢
App(σ, τ, λ(σ, τ, m), n) = m(n)

Notice, how terms with free variables are represented as framework abstractions (in the type of λ) and how substitution is represented as framework application (in the type of App and in the equation).

In this way the burden of dealing correctly with variables, substitution, and binding is shifted from the object language to the Logical Framework and so can be handled once and for all.

Of course, the LF can also cope with type formers other than the dependent function space. Since we refer to it later in §4, we consider here an ad hoc type former (creating a copy of its argument) defined by the two rules

\frac{Γ ⊢ σ type}{Γ ⊢ L(σ) type}  \frac{Γ ⊢ M : σ}{Γ ⊢ l(M) : L(σ)}

In LF it would have to be rendered by two constants L : (Set)Set and l : (σ: Set, σ)L(σ).

The Alf system (Magnusson and Nordström 1994) is based on the Logical Framework. It allows for the definition of types in Set simply by giving their constructors. Functions on the types are then defined by pattern-matching over the constructors as needed.

1In loc. cit. and in the Alf system the type annotations in functional abstractions are omitted. We include them for the sake of consistency.

The Logical Framework can also be used to encode the syntax of other logical systems such as predicate logic and modal logic. The interested reader is referred to (Harper, Honsell, and Plotkin 1993).

2.2.3 The Calculus of Constructions

The Calculus of Constructions (CC) (Coquand and Huet 1988) is a type theory with Π-types and a universe closed under impredicative quantification (U-Impr). The universe is traditionally denoted by Prop and the corresponding El-operator is either written Prf (−) or omitted. The idea is that the universe Prop corresponds to a type of propositions and that Prf (−) associates the type of proofs to a proposition. Originally, it was intended that Prop not only contains propositions, but also datatypes like the natural numbers which are definable by their “impredicative encodings”, for instance one has

Nat =^{def} Prf (∀c: Prop.∀z: Prf (c).∀s: Prf (c) → Prf (c).c)

and for this type constants 0 and Suc(−) can be defined as well as an operator permitting definition of functions by primitive recursion. The point is that Nat itself is of the form Prf (−) and so can serve as the argument c to an element of Nat. Also other inductive datatypes like lists or trees can be defined in this way. Similarly, logical connectives can be defined on the type Prop by their usual higher-order encodings (Coquand and Huet 1988).

The encoding of datatypes inside Prop proved insufficient as no internal induction principles (like R^{N}) are available for these. This gave rise to two extensions of the pure Calculus of Constructions: Luo’s Extended Calculus of Constructions (ECC) implemented in the Lego system (Luo 1994; Luo and Pollack 1992) and the Calculus of Inductive Definitions (CID) implemented in the Coq system (Coquand and Paulin-Mohring 1989; Dowek et al. 1991). ECC extends the Calculus of Constructions by a sequence of universes U_{0}, U_{1}, … where each U_{i+1} contains a code for U_{i} and Prop is contained in U_{0}. Datatypes reside in U_{0} and are given by inductive rules like the ones for N. The higher universes are used for modularisation as hinted at in the example above. Prop is used for propositions only.

In the CID we have two universes both closed under impredicative quantification, Set and Prop. The datatypes reside in Set and are given by inductive rules as in ECC. The implementation of the CID, Coq, comes with a program extraction facility which extracts executable ML programs from derivations in CID essentially by removing all terms and types coming from the universe Prop, see also (Paulin-Mohring 1989).

2.3 Pre-syntax

The syntax of types, terms, and contexts has been given together with the typing and equality rules. For certain purposes it is convenient to have a simpler inductive definition of possibly non well-typed terms, out of which the actual ones are singled out by the rules. For instance, we might want to consider App_{[x:N]N}(0, 0) as a term albeit not a well-typed one. These preterms, -types, and -contexts have been used to give semantics to type theory in terms of untyped computation (Allen 1987; Martin-Löf 1984); we will use them as an auxiliary device in the definition of the interpretation of type theory in semantic structures and also in the definition of context morphisms below.

The pre-contexts (Γ), pre-types (σ, τ), and pre-terms (M, N) for a type theory with Π−, Σ−, identity types, and natural numbers are given by the following grammar.

Γ  ::= ⋄

| Γ, x: σ provided x is not declared in Γ

σ, τ  ::= Πx: σ.τ | Σx: σ.τ | Id_{σ}(M, N) | N
M, N, H, P ::= x | λx: σ.M^{τ} | App_{[x:σ]τ}(M, N) |

Pair_{[x:σ]τ}(M, N) | R_{[z:(Σx:σ.τ)]ρ}^{Σ}([x: σ, y: τ]H, M) | Refl_{σ}(M) | R_{[x:σ,y:σ,p:Id_{σ}(x,y)]|τ}^{Id}([z: σ]H , M, N, P) | 0 | Suc(M) | R_{[n:N]σ}^{N}(H_{z}, [n: N, x: σ]H_{s}, M)

Capture-free substitution and identification of terms with different bound variables can then be dealt with on the level of the pre-syntax. We will use the predicates well-formed or valid for those pre-terms/-types/-contexts which actually occur in derivable judgements. Note that the variables declared in a pre-context are pairwise distinct.

Exercises

E2.1 Construct an inhabitant of the type

m: N, n: N ⊢ Id_{N}(m + n, n + m) type

E2.2 Show that for arbitrary types Γ ⊢ σ type, Γ ⊢ τ type, and Γ, x: σ, y: τ ⊢ ρ type the following type corresponding to the axiom of choice is inhabited:

Γ ⊢ (Πx: σ.Σy: τ.ρ) ⇒ (Σf: σ ⇒ τ.Πx: σ.ρ[(f x)/y]) type

E2.3 By analogy to the type of natural numbers define the rules for a list type former which to any type σ associates a type List(σ) consisting of finite sequences of elements of σ. Hint: think of lists as inductively generated from the empty list by successive additions of elements of σ (“cons”). Define a length function of type List(σ) → N and define a type Vec_{σ}(M) of lists of length M for each M : N using lists, the identity type, and the Σ-type.

E2.4 Define a type of binary natural numbers with three constructors: Zero, Suc_{0}, and Suc_{1} and define a conversion function from these binary representations to N.

E2.5 Give the rules for a universe U containing a code ˆ0 for the empty type 0 and a code ˆ1 for the unit type 1. Show that in a type theory which supports natural numbers, this universe, and the empty type itself the following type in the empty context is inhabited

⋄ ⊢ Id_{N}(0, Suc(0)) → 0 type

corresponding to Peano’s fourth axiom 0 ≠ 1. Hint: define using R^{N} a function f: N → U such that ⋄ ⊢ f0 = ˆ1 : U and ⋄ ⊢ f(Suc(0)) = ˆ0 : U . Later on we will show by a semantic argument that the above type is not inhabited in the absence of a universe (Smith 1988).

E2.6^{∗} (Troelstra and van Dalen 1988) Show that in type theory without the empty type 0 such an empty type can be defined as Id_{N}(0, Suc(0)). The elimination operator R_{σ}^{0} must then be defined by induction on the structure of σ. Notice that in view of the semantic result anticipated in the previous exercise this definition hinges on the fact that there is no empty type in the first place.

E2.7^{∗} Show that for any type theory containing some or all of the type formers described above the rules Weak and Subst are admissible.

E2.8^{∗} (Weak Σ-types in the Calculus of Constructions) For ⊢ σ type and x: σ ⊢ T : Prop define

∃x: σ.P =^{def} ∀c: Prop.(∀x: σ.P ⇒ c) ⇒ c

where X ⇒ Y abbreviates ∀p: Prf (X).Y. Define a pairing operation which to M: σ and N: Prf (P [M]) associates an element ∃-I(M, N) : Prf (∃x: σ.P) and define in the case that σ = Prf (S) for some S: Prop a first projection witness_{S} : Prf (∃x: Prf (S).T) → Prf (S). Show that for M and N as above one has ⊢ witness_{S} ∃-I(M, N) = M.

E2.9 Give the rules for a universe closed under impredicative quantification using the “economic syntax” exemplified in rule U-Π-Ty

E2.10^{∗} Prove that whenever Γ ⊢ M : σ and Γ ⊢ M : τ then Γ ⊢ σ = τ type by induction on derivations. Find some type annotations in term formers which can safely be omitted without violating this property. Discuss the properties a type theory must have so that the type annotation in application can be omitted. In other words when can we replace App_{[x:σ]τ}(M, N) by App(M, N) in the official syntax without violating uniqueness of types. See (Streicher 1991) for a thorough discussion of this point.

2.4 Context morphisms

Definition 2.11 Let Γ and Δ =^{def} x_{1}: σ_{1}, …, x_{n}: σ_{n} be valid contexts. If f =^{def} (M_{1}, …, M_{n}) is a sequence of n pre-terms we write

Γ ⊢ f ⇒ Δ

and say that f is a context morphism from Γ to Δ if the following n judgements hold:

Γ ⊢ M_{1} : σ_{1}
Γ ⊢ M_{2} : σ_{2}[M_{1}/x_{1}]
…
Γ ⊢ M_{n} : σ_{n}[M_{1}/x_{1}][M_{2}/x_{2}] … [M_{n−1}/x_{n−1}]

Examples. For any context Γ we have the empty context morphism () from Γ to ⋄ and this is the only context morphism from Γ to ⋄. If Γ ≡ x_{1}: σ_{1}, …, x_{n}: σ_{n} is a context and Γ ⊢ σ type and x is a fresh variable, then (x_{1}, … x_{n}) forms a context morphism from Γ, x: σ to Γ which we denote by p(Γ, σ). A more concrete example is (0, Refl_{N}(0)) which forms a context morphism from ⋄ to n: N, p: Id_{N}(0, n) as ⋄0: N and ⋄Refl_{N}(0) : (Id_{N}(0, n))[0/n]. The same sequence of terms also forms a context morphism from ⋄ to n: N, p: Id_{N}(0, 0) which shows that the “target context” Δ is not uniquely determined by f. For any term Γ ⊢ M : σ we can form a context morphism Γ ⊢ \overline{M} ⇒ Γ, x: σ where \overline{M} ≡ (x_{1}, …, x_{n}, M) if Γ ≡ x_{1}: σ_{1}, …, x_{n}: σ_{n}. Finally, we have the identity context morphism Γ ⊢ id_{Γ} ⇒ Γ given by id_{Γ} ≡ (x_{1}, …, x_{n}).

2.4.1 Generalised substitution

We denote syntactic identity up to renaming of variables by ≡. If Γ ⊢ f ⇒ Δ and τ is a pre-type we write τ[f/Δ] for the simultaneous replacement of the Δ-variables in τ by the corresponding terms in f, more precisely, if Δ ≡ x_{1}: σ_{1}, …, x_{n}: σ_{n} and f ≡ (M_{1}, …, M_{n}) then

τ[f/Δ] ≡ τ[M_{1}/x_{1}][M_{2}/x_{2}] … [M_{n}/x_{n}]

The attribute “simultaneous” means that the variables in Δ should be made disjoint from those in Γ before performing the substitution. We define −[f/Δ] analogously for pre-terms, pre-contexts, and judgements J of the form M : σ, σ type, M = N : σ, σ = τ type.

By induction on the length of Δ and using rules Weak and Subst we can then establish the following property:

Proposition 2.12 If Γ ⊢ f ⇒ Δ and Δ, Θ ⊢ J then Γ, Θ[f/Δ] ⊢ J [f/Δ].

One is only interested in the case where Θ ≡ ⋄ as this subsumes the general case with f replaced by the context morphism q(f, Θ) from Γ, Θ[f/Δ] to Δ, Θ given by q(f, Θ) ≡ (f, z_{1}, …, z_{k}) for Θ ≡ z_{1}: θ_{1}, …, z_{k}: θ_{k}. However, in order to get the inductive argument through one needs the case of non-empty Θ. When Θ ≡ ⋄ and when no confusion can arise we write τ[f] for τ[f/Δ] and similarly for terms, contexts, and judgements.

Notice the special case of the context morphism p(Γ, σ) defined above. If Γ ⊢ J then Γ, x: σ ⊢ J [p(Γ, σ)], but J ≡ J [p(Γ, σ)] so the generalised substitution subsumes weakening. Similarly, for Γ, x: σ ⊢ J and Γ ⊢ M : σ we have J [\overline{M}] ≡ J [M/x] so ordinary substitution is subsumed, too.

The defined substitution operation allows us to establish the following derived typing rule for non-empty context morphisms:

\frac{Γ ⊢ f ⇒ Δ  ⊢ Δ, x: σ ctxt Γ ⊢ M : σ[f]}{Γ ⊢ (f, M) ⇒ Δ, x: σ} Mor-Cons

This rule together with

\frac{⊢ Γ ctxt}{Γ ⊢ () ⇒ ⋄} Mor-Empty

generates all valid judgements of the form Γ ⊢ f ⇒ Δ.

If Γ ⊢ f ⇒ Δ and Δ ⊢ g ⇒ Θ where g ≡ (N_{1}, …, N_{k}) we can form the list of terms g ∘ f ≡ (N_{1}[f], …, N_{k}[f]). In other words g ∘ f is obtained by simultaneously replaceming the Δ-variables in g by the corresponding terms in f. This list g ∘ f forms a context morphism from Γ to Θ and ∘ as indicated is an associative operation. Although this can be seen directly with some intuition about substitutions we prefer to state it as a proposition together with some other properties which the reader is invited to prove by simultaneous induction on the length of g.

Proposition 2.13 Assume B ⊢ e ⇒ Γ, Γ ⊢ f ⇒ Δ, and Δ ⊢ g ⇒ Θ. Furthermore let Θ ⊢ σ type and Θ ⊢ M : σ. Then the following equations hold up to syntactic identity.

Γ ⊢ g ∘ f ⇒ Θ
σ[g ∘ f] ≡ σ[g][f]
M[g ∘ f] ≡ M[g][f]
(g ∘ f) ∘ e ≡ g ∘ (f ∘ e)

Hint for the proof: define g ∘ f inductively by () ∘ f =^{def} () and (g, M) ∘ f =^{def} (g ∘ f, M[f]) where (g, M) denotes the list g extended by M. Use the fact that τ[f] ≡ τ if none of the Δ-variables occurs in τ and that τ[N/x][f] ≡ τ[f/Δ][N[f]/x]. □

2.4.2 Context morphisms and definitional equality

Let f ≡ (M_{1}, …, M_{n}) and g ≡ (N_{1}, …, N_{n}). If Γ ⊢ f ⇒ Δ and Γ ⊢ g ⇒ Δ then we write Γ ⊢ f = g ⇒ Δ as an abbreviation for the n judgements Γ ⊢ M_{1} = N_{1} : σ_{1}, Γ ⊢ M_{2} = N_{2} : σ_{2}[M_{1}/x_{1}], …, Γ ⊢ M_{n} = N_{n} : σ_{n}[M_{1}/x_{1}] … [M_{n−1}/x_{n−1}] if Δ ≡ x_{1}: σ_{1}, …, x_{n}: σ_{n}. Notice that we could equivalently replace the second judgement by Γ ⊢ M_{2} = N_{2} : σ_{2}[N_{1}/x_{1}] in view of the first one and the congruence rules for definitional equality. If Γ ⊢ f = g ⇒ Δ we say that f and g are definitionally equal context morphisms from Γ to Δ. By straightforward induction it is now possible to derive congruence rules for the defined operators on context morphisms, w.r.t. this definitional equality and we also have that if ⊢ Γ = Γ′ ctxt, ⊢ Δ = Δ′ ctxt, and Γ ⊢ f = g ⇒ Δ then Γ′ ⊢ f = g ⇒ Δ′.

Exercises

E2.14 Show that the above-defined context morphisms p(Γ, σ), \overline{M}, and q(f, Θ) have the following properties:

• If Γ ⊢ f ⇒ Δ then id_{Δ} ∘ f ≡ f ≡ f ∘ id_{Γ}.

• If Γ ⊢ M : σ then p(Γ, σ) ∘ \overline{M} ≡ id_{Γ}.

• If Γ ⊢ (f, M) ⇒ Δ, x: σ then p(Γ, σ) ∘ (f, M) ≡ f and x[(f, M)] ≡ M.

• If Γ ⊢ f ⇒ Δ and ⊢ Δ, x: σ ctxt then p(Δ, σ) ∘q(f, x: σ) ≡ f ∘p(Γ, σ[f]).

• If Γ ⊢ f ⇒ Δ and Δ ⊢ M : σ then \overline{M} ∘ f ≡ q(f, x: σ) ∘ \overline{M[f]}.

• If Γ ⊢ σ type and x fresh then id_{Γ,x:σ} ≡ (p(Γ, σ), x).

E2.15 Show that if Δ ⊢ Πx: σ.τ type and Γ ⊢ f ⇒ Δ then (Πx: σ.τ)[f] ≡ Πx: σ[f].τ[q(f, x: σ)]. Hint: you may assume that x does not occur in Δ as types are identified up to renaming of bound variables.

3 Category-theoretic semantics of type theory

Now we develop an abstract notion of semantics for theories of dependent types of which most known interpretations of type theory form an instance.

The main purpose in defining such an abstract semantics is that it is easier to show that a mathematical structure forms an instance of the abstract framework rather than defining an interpretation function for it directly. This is achieved by essentially three properties of the abstract semantics:

• Substitution is a primitive operation rather than inductively defined.

• Variables are replaced by combinators for substitutions.

• Definitional equality is modelled by true (set-theoretic) equality.

Category-theoretic semantics is based on an abstraction from the combinators (like ∘, p, (−, −), q(−, −)) and equations for context morphisms identified in the previous section. The key concept is the one of a category: a collection of objects (the contexts), and for any two objects a collection of morphisms (the context morphisms) together with an associative composition and identities. For lack of space we cannot give an introduction to categories here and need to presuppose some very basic notions, in particular categories, functors, natural transformations, isomorphisms, terminal objects, and the category of sets and functions. Reading the relevant parts of the first chapter of (Lambek and Scott 1985), for instance, should suffice to attain the required state of knowledge. If C is a category we write |C| or C for its collection of objects and C(A, B) for the collection of morphisms from A to B. We also write f : A → B instead of f ∈ C(A, B). A final prerequisite: if ϕ is an informal proposition then we define the set [ϕ] by [ϕ] ≡ {⋆} if ϕ is true and [ϕ] ≡ ∅ if ϕ is false.

3.1 Categories with families

We choose the semantic framework of categories with families (CwFs) (Dybjer 1996) a variant of Cartmell’s categories with attributes which have the advantage of being equationally defined, rather than using conditional equations. Furthermore, CwFs are closer to the syntax than categories with attributes and therefore—this is the hope of the author—should be easier to understand.

The definition of a CwF follows the structure of the judgements in type theory except that context morphisms and substitution are part of the structure rather than defined afterwards. Along with the explanation of CwFs we define two important instances: the term model T of the calculus of dependent types described in § 2. and the set-theoretic model Set as running examples.

If we include context morphisms the syntax contains four kinds of objects: contexts, context morphisms, types, and terms. Accordingly, for each of these we have a domain of interpretation in the model. More precisely, a CwF C contains • a category C of semantic contexts and context morphisms

• for Γ ∈ C a collection Ty_{C}(Γ) of semantic types

• for Γ ∈ C and σ ∈ Ty_{C}(Γ) a collection Tm_{C}(Γ, σ) of semantic terms

Where appropriate we leave out the attribute “semantic” and write Tm_{C}(σ) instead of Tm_{C}(Γ, σ). We also omit the subscripts if they are clear from the context.

In the term model T the collection of contexts is the quotient by definitional equality of well-formed contexts, that is pre-contexts Γ such that ⊢ Γ ctxt. Two such contexts Γ and Δ are identified if ⊢ Γ = Δ ctxt. We tend to denote equivalence classes by their representatives. A morphism from Γ to Δ is an equivalence class with respect to definitional equality of syntactic context morphisms Γ ⊢ f ⇒ Δ. This is well-defined in view of the observations in §2.4.2. Composition and identities are given by the corresponding operations on syntactic context morphisms. Ty_{T} (Γ) is the set of pre-types σ such that Γ ⊢ σ type again factored by definitional equality, that is σ and τ are identified if Γ ⊢ σ = τ type. Finally, Tm(Γ, σ) is the set of pre-terms M with Γ ⊢ M : σ factored by definitional equality.

The set-theoretic model Set has as category of contexts the category of sets and functions. An element of Ty_{Set}(Γ) is a family of sets (σ_{γ})_{γ∈Γ} indexed over Γ. An element of Tm_{Set}(Γ, σ) is an assignment of an element M(γ) of σ_{γ} for each γ ∈ Γ.

Next, we need constants and operations on these domains in order to interpret the rules of type theory. Moreover, substitution must be axiomatised in such a way that it corresponds to the defined syntactic substitution. The definition of CwFs only accounts for the structural rules common to all systems of dependent types as set out in § 2. The interpretation of the various type and term formers will be given afterwards as additional structure.

Semantic substitution is described by two operations for each context morphism, one for types and one for terms: if f : Γ → Δ then there is a function −{f} : Ty(Δ) → Ty(Γ) and for σ ∈ Ty(Δ) a function −{f} : Tm(Δ, σ) → Tm(Γ, σ{f}). These operations must be compatible with composition and identities in the following sense. If Γ, Δ, Θ ∈ C, f : Γ → Δ, g : Δ → Θ, σ ∈ Ty(Θ), and M ∈ Tm(Θ, σ) then the following equations are required to hold:

σ{id_{Θ}} =  σ  ∈ Ty(Θ)  (Ty-Id)
σ{g ∘ f} = σ{g}{f} ∈ Ty(Γ)  (Ty-Comp)
M{id_{Θ}} = M ∈ Tm(Θ, σ) (Tm-Id)
M{g ∘ f} = M{g}{f} ∈ Tm(Γ, σ{g ∘ f})  (Tm-Comp)

Notice that the former two equations are required for the two latter to “typecheck”. Notice also, that substitution together with equations (Ty-Id) and (Ty-Comp) makes Ty a contravariant functor from C to Set. The sets Tm can also be organised into a functor, see §3.1.1 below.

In the term model substitution is the “generalised substitution” defined in §2.4.1. This means that we have σ{f} =^{def} σ[f] and M{f} =^{def} M[f]. In the set-theoretic model substitution is given by pre-composition. If f : Δ → Γ is a function and (σ_{γ})_{γ∈Γ} is a family of sets then σ{f} is the family of sets given by σ{f}_{δ} =^{def} σ_{f(δ)}. Similarly, if M ∈ Tm(Γ, σ) then M{f}(δ) =^{def} M(f(δ)). It is easy to see that the required equations hold.

Next we want to interpret the context formation rules. To model the empty context we require a terminal object ⊤ in the category C. We usually write ⟨⟩_{Γ} for the unique morphism from Γ to ⊤. In the term model and in the set-theoretic model these terminal objects are the empty context and an arbitrary singleton set, respectively.

To interpret context extension we require for each Γ ∈ C and σ ∈ Ty(Γ) a context Γ.σ ∈ C and a morphism p(σ) : Γ.σ → Γ. The context Γ.σ is called the comprehension of σ and p(σ) is called the projection associated to σ. In the term model Γ.σ is the extended context Γ, x: σ and p(σ) is the context morphism given by Γ, x: σ ⊢ p(Γ, σ) ⇒ Γ as defined in §2.4. In the set-theoretic model Γ.σ is the disjoint union of the σ_{γ}, i.e. the set { (γ, x) | γ ∈ Γ ∧ x ∈ σ_{γ} }. The function p(σ) then sends (γ, x) to γ.

The morphism p(σ) can be seen as the first projection out of the generalised product Γ.σ. The second projection takes the form of an element v_{σ} ∈ Tm(Γ.σ, σ{p(σ)}) corresponding to the judgement Γ, x: σ ⊢ x : σ.

In the term model this is the term x in Γ, x: σ ⊢ x : σ, whereas in the set-theoretic model we define it by the assignment (γ, x) ↦ x. Note that, in this model, σ{p(σ)}_{(γ,x)} = σ_{γ}.

According to the definition of syntactic context morphisms we need an operation which extends a semantic context morphism by a terms. If f : Γ → Δ, σ ∈ Ty(Δ), and M ∈ Tm(Γ, σ{f}) then there is a context morphism ⟨f, M⟩_{σ} : Γ → Δ.σ—the extension of f by M—satisfying the following equations for f : Γ → Δ, g : B → Γ, σ ∈ Ty(Δ), M ∈ Tm(Γ, σ{f}).

p(σ) ∘ ⟨f, M⟩_{σ} =  f  : Γ → Δ  (Cons-L)
v_{σ}{⟨f, M⟩_{σ}} =  M  ∈ Tm(Γ, σ{f})  (Cons-R)
⟨f, M⟩_{σ} ∘ g = ⟨f ∘ g, M{g}⟩_{σ} : B → Δ.σ  (Cons-Nat)
⟨p(σ), v_{σ}⟩_{σ} =  id_{Δ.σ}  : Δ.σ → Δ.σ  (Cons-Id)

In the term model the extension of f by M is Γ ⊢ (f, M) ⇒ Δ, x: σ, whereas in the set-theoretic model we have ⟨f, M⟩_{σ}(γ∈ Γ) =^{def} (f(γ), M(γ)). We include the “type” information σ in ⟨f, M⟩_{σ} as it cannot be inferred from the “types” of f and M.

This completes the definition of categories with families. Let us summarise that a CwF is a structure (C, Ty, Tm, −{−}, ⊤, ⟨⟩_{−}, −.−, p, v_{−}, ⟨−, −⟩_{−}) of sorts and operations subject to the requirements set out above. (The substitution −{−} is understood to work for both types and terms.)

3.1.1 A more abstract definition

We give in this section an equivalent, but more abstract and more compact definition of CwF based on family-valued functors and a universal property. The idea of using family-valued functors is due to Peter Dybjer.

Definition 3.1 The category Fam of families of sets has as objects pairs B = (B^{0}, B^{1}) where B^{0} is a set and (B_{b}^{1})_{b∈B^{0}} is a family of sets indexed over B^{0}. A morphism from B to C = (C^{0}, C^{1}) is a pair (f^{0}, f^{1}) where f^{0} : B^{0} → C^{0} is a function and f^{1} = (f_{b}^{1})_{b∈B^{0}} is a family of functions f_{b}^{1} : B^{1}(b) → C^{1}(f^{0}(b)).

The carrier sets Ty and Tm of a CwF over category C can now be given more compactly as a single functor F : C^{op} → Fam. Indeed, given Ty and Tm we obtain a functor functor F with object part

F(Γ) = (Ty(Γ), (Tm(Γ, σ))_{σ∈Ty(Γ)})

The morphism part of F is induced by semantic substitution. Conversely, given a functor F : C^{op} → Fam we define Ty(Γ) := F^{0} and Tm(Γ, σ) = F^{1}(σ) where F(Γ) = (F^{0}, F^{1}). If f : Δ → Γ then writing F(f) = (f^{0}, f^{1}) we have f^{0} : Ty(Γ) → Ty(Δ) and f_{σ}^{1} : Tm(Γ, σ) → Tm(Δ, f^{0}(σ)) giving us semantic substitution. The required equations follow from functoriality of F.

Definition 3.2 Let C be a category and F = (Ty, Tm) : C^{op} → Fam be a functor. Furthermore, let Γ be an object of C and σ ∈ Ty(Γ). A comprehension of σ is given by an object Γ.σ of C together with two projections p(σ) : Γ.σ → Γ and v_{σ} ∈ Tm(Γ.σ, σ{p(σ)}) such that for each f : Δ → Γ and M ∈ Tm(σ{f}) there exists a unique morphism ⟨f, M⟩_{σ} : Δ → Γ.σ satisfying p(σ) ∘ ⟨f, M⟩_{σ} = f and v_{σ}{⟨f, M⟩_{σ}} = M.

Definition 3.3 (Dybjer) A category with families is given by the following data.

• a category C with terminal object,

• a functor F = (Ty, Tm) : C^{op} → Fam,

• a comprehension for each Γ ∈ C and σ ∈ Ty(Γ).

This definition is equivalent to the one in §3.1. The proof is left to the reader.

The fact that comprehensions enjoy a universal property and thus are unique up to isomorphism (see E3.12) means that up to a choice of representatives a CwF is fully determined by its underlying family-valued functor.

3.1.2 Terms and sections

Assume a CwF. If M ∈ Tm(Γ, σ) then also M ∈ Tm(Γ, σ{id_{Γ}}) and thus

\overline{M} =^{def} ⟨id_{Γ}, M⟩_{σ} : Γ → Γ.σ

By (Cons-L) we have p(σ) ∘ \overline{M} = id_{Γ} thus \overline{M} is a right inverse or a so-called section of p(σ). Conversely, if f : Γ → Γ.σ is a section of p(σ), that is, p(σ) ∘ f = id_{Γ} then

v_{σ}{f} ∈ Tm(Γ, σ{p(σ)}{f}) = Tm(Γ, σ{p(σ) ∘ f}) = Tm(Γ, σ)

by (Ty-Comp), (Ty-Id), and assumption. These two operations establish a bijective correspondence between the collection Sect(p(σ)) of sections of p(σ) and Tm(Γ, σ), as v_{σ}\{M̄\} = M by (Cons-L) and \overline{v_{σ}\{f\}} = ⟨id_{Γ}, v_{σ}\{f\}⟩_{σ} = ⟨p(σ) ∘ f, v_{σ}{f}⟩_{σ} = ⟨p(σ), v_{σ}⟩_{σ} ∘ f = f by (Cons-Nat) and (Cons-Id).

3.1.3 Weakening

Suppose that f : B → Γ and σ ∈ Ty(Γ). A context morphism q(f, σ) : B.σ{f} → Γ.σ called the weakening of f by σ is defined by

q(f, σ) = ⟨f ∘ p(σ{f}), v_{σ{f}}⟩_{σ}

In the term model q(f, σ) is the eponymous syntactic context morphism defined in §2.4; in the set-theoretic model we have q(f, σ)(β∈ B, x∈ σ_{f(β)}) = (f(β), x).

A weakening map is a morphism of the form p(σ) : Γ.σ → Γ or (inductively) a morphism of the form q(w, τ) where w is a weakening map. In the term model a weakening map takes the form of a projection from Γ, x: σ, Δ to Γ, Δ.

We introduce the abbreviations σ^{+} and M^{+} for σ{w} and M{w} if w is a weakening map which is clear from the context. Furthermore, if f : Γ → Δ is any context morphism we may write f^{+} for q(f, σ). For example, as demonstrated in E2.15 we have in the term model Πx: σ.τ{f} = Πx: σ{f}.τ{f^{+}}.

Exercises

E3.4 Show that in a CwF the defined morphisms q(f, σ) from §3.1.3 do satisfy the coherence requirements q(id_{Γ}, σ) = id_{Γ.σ} and q(f ∘ g, σ) = q(f, σ) ∘ q(g, σ{f}).

E3.5 Transform the following equations into the explicit notation; prove them, and explain their intuitive meaning. (1) p(σ)^{+} ∘ \overline{v_{σ}} = p(σ^{+}) ∘ \overline{v_{σ}} = id_{Γ.σ};

(2) f^{+} ∘ \overline{M\{f\}} = \overline{M} ∘f; (3) f = ⟨p(σ) ∘f, v_{σ}\{f\}⟩_{σ}. Also expand the expression Γ.σ.τ when σ, τ ∈ TyΓ.

E3.6 Check that equations (Cons-L) … (Cons-Id) hold in the set-theoretic model.

E3.7 This exercise will be taken up in later sections and will lead us up to Jan Smith’s proof of the independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes (Smith 1988). Let P be the poset of truth values {ff, tt} where ff ≤ tt viewed as a category. Show that P has a terminal object, viz. tt. Extend P to a CwF by putting Ty_{P}(tt) = Ty_{P}(ff) = {ff, tt} and Tm_{P}(Γ, σ) = [Γ ≤ σ]. Hint: define comprehension by Γ.σ =^{def} Γ ∧ σ. An intuition for this model (or rather for the interpretation of the syntax in it) is to view tt as “potentially inhabited” and ff as “always empty”.

3.2 Other notions of semantics

In the literature other notions of model have been offered which mostly are equivalent to CwFs. A key property of these models is that substitution on terms is a defined concept rather than a primitive. To understand how this works we need the notion of pullback in a category.

Definition 3.8 Let C be a category, f : X → Y and g : Z → Y morphisms with common codomain. A pullback of g along f is a pair of morphisms p : P → Y and q : P → Z such that f ∘ p = g ∘ q and whenever p′ : P′ → X and q′ : P′ → Z are two morphisms with f ∘ p′ = g ∘ q′ then there exists a unique morphism h : P′ → P such that p ∘ h = p′ and q ∘ h = q′. ^{2}

P′
[figure: p′; q′; ..............; h]
P  \overline{q ^{}}Z

[figure: X; p; f; Y; g]

A quadruple (p, q, f, g) of morphisms with f ∘ p = g ∘ q (a commuting square) is called a pullback if p and q form a pullback of g along f.

In the category Set the pullback of g : Z → Y along g : X → Y always exists and is (e.g.) given by P =^{def} {(x, z) | x ∈ X ∧ z ∈ Z ∧ f(x) = g(z)}. The two projections p, q send a pair (x, z) ∈ P to x and z, respectively.

2This and the following diagrams were typeset using Paul Taylor’s Latex diagram package the use of which is herewith gratefully acknowledged.

In Set we can view a morphism g : Z → Y as a family of sets indexed over Y, namely the family of sets (g^{−1}(y))_{y∈Y} where g^{−1}(y) =^{def} {z ∈ Z | g(z) = y}. Conversely, if we are given a family of sets (G_{y})_{y∈Y} we can construct a function g into Y as the projection from the disjoint union

Z =^{def} {(y, γ) | y ∈ Y ∧ γ ∈ G_{y}}

to Y which sends (y, γ) to y. (This is precisely p((G_{y})_{y∈Y}) in the notation of §3.1.) Now a pullback of the thus defined g : Z → Y along f : X → Y is given by applying this construction to the composite family (G_{f(x)})_{x∈X}, more precisely, we can put

P =^{def} {(x, γ) | x ∈ X ∧ γ ∈ G_{f(x)}}

with projections p(x, γ) = x and q(x, γ) = (f(x), γ). Note that this is not equal to the canonical pullback of g along f which is {(x, (x′, γ)) | x = x′ and γ ∈ G_{f(x′)}}.

A more general correspondence between pullbacks and substitution arises in the framework of CwFs:

Proposition 3.9 Let C be a CwF, f : B → Γ, and σ ∈ Ty(Γ). The following square is a pullback

[figure: B.σ{f}; q(f, σ); Γ.σ; B; p(σ{f}); f; Γ; p(σ)]

Proof. The diagram commutes by equation (Cons-L). To see that it is indeed a pullback assume p′ : Θ → B and q′ : Θ → Γ.σ such that f ∘p′ = p(σ) ∘q′. We can decompose q′ as q′ = ⟨p(σ), v_{σ}⟩_{σ} ∘ q′ = ⟨p(σ) ∘ q′, v_{σ}{q′}⟩_{σ} = ⟨f ∘ p′, N⟩_{σ},

where N =^{def} v_{σ}{q′}. We have N ∈ Tm(σ{p(σ)}{q′}) = σ{p(σ) ∘ q′} = σ{f ∘

p′} = σ{f}{p′}. Therefore,

h =^{def} ⟨p′, N⟩_{σ{f}} : Θ → B.σ{f}

We have p(σ{f}) ∘ h = q′ by (Cons-L) and

q(f, σ) ∘ h
= ⟨f ∘ p(σ{f}), v_{σ{f}}⟩_{σ} ∘ h  by definition
= ⟨f ∘ p(σ{f}) ∘ h, v_{σ{f}}{h}⟩_{σ}  by (Cons-Nat)
= ⟨f ∘ p′, v_{σ{f}}{h}⟩_{σ}  by (Cons-L)
= ⟨f ∘ p′, v_{σ}{q′}⟩_{σ}  by (Cons-R)
= ⟨p(σ) ∘ q′, v_{σ}{q′}⟩_{σ}  by assumption
= q′  by (Cons-Nat) and (Cons-Id)

For uniqueness assume a morphism h′ : Θ → B.σ{f} such that p(σ{f})∘h′ = p′ and q(f, σ) ∘ h′ = q′. We must show h′ = h. To see this, we expand h′ as ⟨p(σ{f}) ∘ h′, v_{σ{f}}{h′}⟩_{σ{f}} using (Cons-Id), (Id-L), (Cons-Nat). By assumption we can rewrite this to ⟨p′, M⟩_{σ{f}} where

M =^{def} v_{σ{f}}{h′} ∈ Tm(σ{f ∘p(σ{f})∘h′}) = Tm(σ{f ∘p′}) = Tm(σ{p(σ)∘q′})

Now we have

v_{σ}{q′}
= v_{σ}{q(f, σ) ∘ h′}  by assumption
= v_{σ{f}}{h′}  by definition of q and (Cons-R)
= M

so we are done. □

The pullback property of substitution may be taken as primitive thereby making substitution on terms superfluous.

Definition 3.10 A category with attributes (Cartmell 1978; Moggi 1991; Pitts 1997) consists of

• A category C with terminal object ⊤.

• A functor Ty : C^{op} → Set, i.e., a set Ty(Γ) for each Γ ∈ C and a function −{f} : Ty(Γ) → Ty(B) for each f : B → Γ such that (Ty-Id) and (Ty-Comp) from §3.1 hold.

• For each σ ∈ Ty(Γ) an object Γ.σ and a morphism p(σ) : Γ.σ → Γ.

• For each f : B → Γ and σ ∈ Ty(Γ) a pullback diagram

[figure: B.σ{f}; q(f, σ); Γ.σ; B; p(σ{f}); f; Γ; p(σ)]

such that q(id_{Γ}, σ) = id_{Γ.σ} and q(f ∘ g, σ) = q(f, σ) ∘ q(g, σ{f}).

It follows from Prop. 3.9 and E3.4 that every CwF is a category with attributes if we forget about the terms.

Conversely, given a category with attributes we can construct a CwF by putting Tm(Γ, σ) =^{def} Sect(p(σ)) and for M ∈ Tm(Γ, σ) defining M{f} as the unique morphism with p(σ{f}) ∘ M{f} = id_{B} and q(f, σ) ∘ M{f} = M ∘ f.

For f : B → Γ, M ∈ Tm(B, σ{f}) we put ⟨f, M⟩_{σ} =^{def} q(f, σ) ∘ M and finally define v_{σ} as the unique morphism v_{σ} : Γ.σ → Γ.σ.σ^{+} with p(σ^{+}) ∘ v_{σ} = p(σ)^{+} ∘ v_{σ} = id_{Γ.σ}. We leave it as an exercise to verify that this defines indeed a CwF.

If one starts out with a category with attributes, constructs a CwF, and from this CwF again a category with attributes one ends up with the one to start off with. The other way round one gets back the original CwF with the set of terms Tm(Γ, σ) replaced by the set of right inverses to p(σ) (cf. §3.1.2).

Notice that context extensions in categories with attributes are not unique up to isomorphism. For instance, if σ ∈ Ty(Γ) nothing prevents us from defining Γ.σ simply as Γ and the corresponding morphisms p and q as identities.

There are various other notions of model all of which are essentially equivalent as far as interpretation of type theory in them is concerned. Locallycartesian closed categories (Seely 1984) and categories with display maps (Taylor 1986; Lamarche 1987; Hyland and Pitts 1989) are less general than CwFs because semantic types are identified with their associated projections. Usually, in these models the conditions corresponding to (Ty-Comp) and (Ty-Id) only hold up to isomorphism, which makes the definition of the interpretation function more complicated. See (Hofmann 1995b; Curien 1993). Models based on fibrations (Jacobs 1991; Jacobs 1993; Ehrhard 1988) and indexed categories (Curien 1989; Obtułowicz 1989) are more general since they allow for morphisms between semantic types. These morphisms make it possible to describe certain type formers more elegantly, but do not have a direct counterpart in the syntax. Mention must also be made of contextual categories where semantic contexts carry an explicit tree structure corresponding to context extensions (see (Streicher 1991; Cartmell 1978) and E3.13).

For a good taxonomy of the different notions and various back-and-forth constructions see (Jacobs 1993).

Exercises

E3.11 (Agnes Diller) Show that the requirement q(id_{Γ}, σ) = id_{Γ.σ} in Def. 3.10 is actually redundant.

E3.12^{∗} Prove that comprehensions are indeed unique up to isomorphism in the following sense: If σ ∈ Ty(Γ) and p : Σ → Γ and v ∈ Tm(σ{f}) is a comprehension of σ then there exists an isomorphism f : Γ.σ → Σ satisfying p ∘ f = p(σ) and v{σ} = v_{σ}.

Now give another proof of Prop. 3.9 by showing that (Θ, p′, v_{σ}{q′}) is a comprehension of σ{f}.

E3.13^{∗} A contextual category (Cartmell 1978; Streicher 1991) is a category C with terminal object ⊤ and a tree structure on the objects given by a function f on the objects of C such that f(⊤) = ⊤ and f (“father”) is injective on C \ {⊤} and for each Γ ∈ C there is a minimal n—the level of Γ—such that f^{n}(Γ) = ⊤. Moreover, the assignment Ty(Γ) = {Δ | f(Δ) = Γ} extends to a category with attributes over C. Spell this out without using the notion of a category with attributes and define a canonical construction of a contextual category out of a CwF. The objects of the contextual category are lists (σ_{1}, ⋯, σ_{k}) where σ_{1} ∈ Ty(⊤) and σ_{i+1} ∈ Ty(⊤.σ_{1}. · · · .σ_{i}).

The advantage of contextual categories is that they rule out semantic contexts which do not arise from the empty context by successive applications of comprehension. This can be used to establish properties of semantic contexts by induction on the level. Examples of this can be found in (Streicher 1991).

E3.14^{∗} Assume a CwF C. For each Γ ∈ C we define a category D(Γ) with objects the types over Γ and in which a morphism from σ to τ is a C-morphism f : Γ.σ → Γ.τ such that p(τ) ∘ f = p(σ). Equivalently a morphism from σ to τ can be defined as an element of Tm(Γ.σ, τ^{+}) (Why?). Explain why this defines indeed a category and find an extension of the assignment D to a contravariant functor from C to the category of categories.

Such a functor is called an indexed category and forms the heart of Curien and Ehrhard’s notion of D-categories (Curien 1989; Ritter 1992).

3.3 Semantic type formers

In order to interpret a type theory in a CwF we must specify how the various type and term formers are to be interpreted. This results in certain requirements on a CwF which follow very closely the syntactic rules. We give a precise definition for closure under Π, Σ, Id, ∀ to convey the general pattern. The reader may then by herself define the conditions for the other type formers. Some are treated in the exercises.

Definition 3.15 A CwF supports Π-types if for any two types σ ∈ Ty(Γ) and τ ∈ Ty(Γ.σ) there is a type Π(σ, τ) ∈ Ty(Γ) and for each M ∈ Tm(Γ.σ, τ) there is a term λ_{σ,τ}(M) ∈ Tm(Γ, Π(σ, τ)) and for each M ∈ Tm(Γ, Π(σ, τ)) and N ∈ Tm(Γ, σ) there is a term App_{σ,τ}(M, N) ∈ Tm(Γ, τ\{\overline{M}\}) such that (the appropriately typed universal closures of) the following equations hold:

App_{σ,τ}(λ_{σ,τ}(M), N) =  M\{\overline{N}\}  Π-C
Π(σ, τ){f}  = Π(σ{f}, τ{q(f, σ)}) ∈ Ty(B)  Π-S
λ_{σ,τ}(M){f}  = λ_{σ{f},τ{q(f,σ)}}(M{q(f, σ)})  λ-S
App_{σ,τ}(M, N){f} = App_{σ{f},τ{q(f,σ)}}(M{f}, N{f}) App-S

The third equation typechecks by virtue of the second. The last equation makes implicit use of (Ty-Comp) and the fact that

q(f, σ) ∘ \overline{M\{f\}} = \overline{M} ∘ f

which follows by rewriting both sides to ⟨f, M{f}⟩_{σ}.

We see that we stipulate exactly the same type and term formers as in the syntax together with an equation corresponding to Π-C. Congruence rules are not needed on the semantic level as everything preserves equality, but we need extra equations to specify that substitution commutes with the semantic type and term formers.

Since substitution is a primitive notion in the semantics we can obtain a more economic definition of dependent function spaces by restricting the App-combinator to variables and replacing it by an appropriate morphism.

Proposition 3.16 A CwF supports dependent function spaces iff there are operations Π and λ as in Def. 3.15 and for any two types σ ∈ Ty(Γ) and τ ∈ Ty(Γ.σ) a morphism

App_{σ,τ} : Γ.σ.Π(σ, τ)^{+} → Γ.σ.τ

such that

p(τ) ∘ App_{σ,τ} = p(Π(σ, τ)^{+}) App-T

and for every term M ∈ Tm(τ)

App_{σ,τ} ∘ \overline{M\{p(σ)\}} = \overline{M} Π-C’

and, finally, for every morphism f : B → Γ

App_{σ,τ} ∘ q(q(f, σ), Π(σ, τ){q(f, σ)}) = q(q(f, σ), τ) ∘ App_{σ{f},τ{q(f,σ)}}

Proof. The first equation states that App_{σ,τ} leaves its first two arguments unchanged, and thus corresponds to a term of τ^{+}. The second equation corresponds to Π-C, and the third one to App-S; stability under substitution. From the App-morphism we can define an application combinator as follows. Given M ∈ Tm(Π(σ, τ)) and N ∈ Tm(σ) then v_{τ}{App_{σ,τ} ∘ ⟨N, M^{+}⟩_{Π(σ,τ)^{+}}} ∈ Tm(τ\{p(τ) ∘App_{σ,τ} ∘⟨N, M^{+}⟩_{Π(σ,τ)^{+}}\} = Tm(τ\{\overline{N}\}) by Eqn. App-T and it follows from the other two equations that this term has the required properties. Conversely, suppose that a model supports dependent function spaces in the sense of Def. 3.15. Let Δ be Γ.σ.Π(σ, τ)^{+}. We have N =^{def} v_{σ}^{+} ∈ Tm(Δ, σ^{++}) and M =^{def} v_{Π(σ,τ)^{+}} ∈ Tm(Δ, Π(σ, τ)^{++}) = Tm(Δ, Π(σ^{++}, τ^{++})). Accordingly, we have

App_{σ,τ}(M, N) ∈ Tm(Δ, τ^{++}{N}) = Tm(Δ, τ^{+})

We define the application morphism as

⟨p(Π(σ, τ)^{+}, App_{σ,τ}(M, N)⟩_{τ}

The verifications are left to the reader. □

This second definition of dependent function spaces allows for the following restriction by which λ_{σ,τ}(M) is required to be the unique element of Tm(Π(σ, τ)) for which Π-C’ holds.

Definition 3.17 A CwF supports Π-types in the strict sense if it supports them and whenever M ∈ Tm(Γ.σ, τ) and U ∈ Tm(Π(σ, τ)) and App_{σ,τ} ∘ \overline{U^{+}} = \overline{M} then U = λ_{σ,τ}(M).

The syntactic counterpart to these strict Π-types is an η-rule which allows one to conclude Γ ⊢ λx: σ.(M x)^{τ} = M : Πx: σ.τ from Γ ⊢ M : Πx: σ.τ.

If Π-types are supported in the strict sense then Eqn. λ-S can be derived. Moreover, the operation Π(σ, −) then becomes part of an adjunction, see, e.g. (Pitts 1997).

The term model of a type theory with Π-types supports Π-types with the obvious settings:

Π(σ, τ) =^{def} Πx: σ.τ

λ_{σ,τ}(M) =^{def} λx: σ.M^{τ}

App_{σ,τ}(M, N) =^{def} App_{[x:σ]τ}(M, N)

The corresponding application morphism is the context morphism defined by Γ, y: σ, z: Πx: σ.τ ⊢ (x⃗, App_{[x:σ]τ}(z, y)) ⇒ Γ, x: σ, w: τ where x⃗ are the variables in Γ. Notice that these Π-types are not strict unless we enrich our type theory with the abovementioned η-equation.

The set-theoretic model supports Π-types in the strict sense. If (σ_{γ})_{γ∈Γ} ∈ Ty(Γ) and (τ_{(γ,x)})_{(γ,x)} ∈ Γ.σ then we define Π(σ, τ)_{γ} =^{def} Π_{x∈σ_{γ}}τ_{(γ,x)} and abstraction and application as their set-theoretic companions.

Definition 3.18 A CwF supports Σ-types if the following data are given:

• for any two types σ ∈ Ty(Γ) and τ ∈ Ty(Γ.σ) there is a type Σ(σ, τ) ∈ Ty(Γ) such that

Σ(σ, τ){f} = Σ(σ{f}, τ{f^{+}}) Σ-S

whenever f : B → Γ.

• A morphism Pair_{σ,τ} : Γ.σ.τ → Γ.Σ(σ, τ) such that p(Σ(σ, τ)) ∘Pair_{σ,τ} = p(σ) ∘ p(τ) and such that

f^{+} ∘ Pair_{σ,τ} = Pair_{σ{f},τ{f^{+}}} ∘ f^{++} Pair-S

whenever f : B → Γ.

• For every type ρ ∈ Ty(Γ.Σ(σ, τ) and term H ∈ Tm(ρ{Pair_{σ,τ}}) a term R_{σ,τ,ρ}^{Σ}(H) ∈ Tm(ρ) such that

R_{σ,τ,ρ}^{Σ}(H){Pair_{σ,τ}} = H Σ-C

and

\begin{matrix}R_{σ,τ,ρ}^{Σ}(H)\{f^{+}\} = \\ R_{σ\{f\},τ\{f^{+}\},ρ\{f^{+}\}}^{Σ}(H\{f^{++}\}) R^{Σ}-S \end{matrix}

The term model supports Σ-types as follows: if Γ, x: σ ⊢ τ type then Σ(σ, τ) =^{def} Σx: σ.τ and Pair_{σ,τ} is the context morphism

Γ, x: σ, y: τ ⊢ (γ, Pair_{[x:σ]τ}(M, N)) ⇒ Γ, z: Σx: σ.τ

Finally, if Γ, x: σ, y: τ ⊢ H : ρ[Pair_{[x:σ]τ}(x, y)] then Γ, z: Σx: σ.τ ⊢ R^{Σ}(H, z) : ρ. Also the set-theoretic model supports Σ-types as follows.

Σ(σ, τ)_{γ∈Γ} =^{def} {(x, y) | x ∈ σ_{γ} ∧ y ∈ τ_{(γ,x)}}

and

Pair_{σ,τ}(γ, x, y) =^{def} (γ, (x, y))

This morphism Pair is surjective and thus we can take Σ-C as the defining equation for R_{σ,τ,ρ}^{Σ} which also ensures that R_{σ,τ,ρ}^{Σ}(H) is the unique term with property Σ-C. Again, we say that Σ-types are supported in the strict sense if this is the case.

Definition 3.19 A CwF supports (intensional) identity types if for each type σ ∈ Ty(Γ) the following data are given:

• a type Id_{σ} ∈ Ty(Γ.σ.σ^{+}),

• a morphism Refl_{σ} : Γ.σ → I(σ) where I(σ) = Γ.σ.σ^{+}.Id_{σ} such that p(Id_{σ}) ∘ Refl_{σ} equals \overline{v_{σ}} : Γ.σ → Γ.σ.σ^{+}; the diagonal morphism,

• for each τ ∈ Ty(I(σ)) a function R_{σ,τ}^{Id} ∈ Tm(τ{Refl_{σ}}) → Tm(τ)

in such a way that these data are stable under substitution w.r.t. morphisms f : B → Γ and such that whenever τ ∈ Ty(I(σ)) and H ∈ Tm(τ{Refl_{σ}}) then R_{σ,τ}^{Id}(H){Refl_{σ}} = H.

The term model of intensional type theory supports identity types with the following settings: if Γ ⊢ σ type then Id_{σ} is the type Γ, x: σ, y: σ ⊢ Id_{σ}(x, y) type and Refl_{σ} is the context morphism

Γ, x: σ ⊢ (γ, x, x, Refl_{σ}(x)) ⇒ Γ, x: σ, y: σ, p: Id_{σ}(x, y)

If Γ, x: σ, y: σ, p: Id_{σ}(x, y) ⊢ τ[x, y, p] type and Γ, x: σ ⊢ H : τ[x, x, Refl_{σ}(x)] then

Γ, x: σ, y: σ, p: Id_{σ}(x, y) ⊢ R^{Id}([x: σ]H, x, y, p) : τ[x, y, p]

which defines the required function.

The set-theoretic model supports identity types with (Id_{σ})_{(γ,x,y)} =^{def} [x = y] and Refl_{σ}(γ, x) =^{def} (γ, x, x, ⋆). For H ∈ Tm_{Set}(τ{Refl_{σ}}) we put

R_{σ,τ}^{Id}(H)(γ, x, y, p) =^{def} H(x)

which is type correct because in the presence of p ∈ Id_{σ}(x, y) we have x = y and furthermore p itself equals ⋆.

The semantic interpretation of natural numbers, unit types, empty types follows the pattern of the Σ-types and is left to the reader. We conclude the definition of semantic analogues to type formers by specifying the interpretation of a universe closed under impredicative quantification.

Definition 3.20 A CwF supports the Calculus of Constructions if it supports Π-types and the following data are given:

• a type Prop ∈ Ty(⊤). We write Prop also for ⊤.Prop,

• A type Prf ∈ Ty(Prop),

• for σ ∈ Ty(Γ) and p : Γ.σ → Prop a morphism ∀_{σ}(p) : Γ → Prop,

• a term former λ_{σ,p}(−) and a morphism App_{σ,p} like in Prop 3.16 establishing that Prf {∀_{σ}(p)} is a dependent function space of Prf {p} over σ

such that all these data are stable under substitution.

The term model is a model for the Calculus of Constructions with Prop equal to the type of propositions Prop in ⋄ ⊢ Prop type and the type of proofs equal to Prf (x) in x: Prop ⊢ Prf (x) type. A morphism from Γ.σ to Prop takes the form of a term Γ, x: σ ⊢ P : Prop. Then Γ ⊢ ∀x: σ.P : Prop is a morphism from Γ to Prop with the required properties.

The set-theoretic model is a model for the Calculus of Constructions with the settings Prop =^{def} {ff, tt} and Prf_{x} =^{def} [x = tt]. If p : Γ.σ → Prop then we define ∀_{σ}(p)(γ) =^{def} [“p(γ, x) = tt for all x ∈ σ_{γ}”].

Notice that in this model all elements of a type Prf (A) are equal. By “Reynolds’ paradox” (Reynolds and Plotkin 1988) this has to be so in any set-theoretic interpretation of the Calculus of Constructions. In §3.4 below we describe a model where this is not the case.

Notice that Prf {∀_{σ}(p)} is not equal to Π(σ, Prf {p}) but in bijective correspondence because if p(γ, x) = tt for each x ∈ σ_{γ} then Prf {∀_{σ}(p)} = {⋆}, whereas Π(σ, Prf {p})_{γ} is the set of functions from σ_{γ} to {⋆} which is a singleton set, but not {⋆}. However, this bijective correspondence enables us to define the required operations λ_{σ,p} and App_{σ,p}.

Exercises

E3.21 Show that the truth value model from E3.7 supports Π and Σ-types each in the strict sense, as well as identity types with the settings Π(σ, τ) =^{def} σ ⊃ τ and Σ(σ, τ) =^{def} σ ∧ τ and Id_{σ} =^{def} tt, where ⊃ and ∧ denote implication and conjunction of truth values.

E3.22^{∗} Show that a CwF supports Σ-types in the strict sense iff it supports them and each morphism Pair_{σ,τ} is an isomorphism.

E3.23 Spell out what it means that Id and Refl are stable under substitution.

E3.24 Explain how a CwF C supports unit types if (but not only if) there exists 1 ∈ Ty(⊤) such that ⊤.1 is a terminal object in C or equivalently ⊤.1 is isomorphic to ⊤.

E3.25 Define what it means for a model to support natural numbers. Show that the set-theoretic model supports natural numbers by N =^{def} ω and that the truth value model supports natural numbers by N =^{def} tt.

E3.26^{∗} Define what it means to support an empty type in the sense of §2.1.7 and show that the set-theoretic model supports it by 0 =^{def} ∅ and that the truth value model supports it by 0 =^{def} ff and that this interpretation is the only possibility. Conclude that if M, N ∈ Tm(Γ, σ) in this model then the set Tm(Γ.Id_{σ}\{⟨\overline{M}, N^{+}⟩_{σ^{+}}\}, 0) is empty.

E3.27 Show that the truth value model forms a model of the Calculus of Constructions with Prop =^{def} tt, Prf (⋆) =^{def} tt, ∀_{σ}(⋆) =^{def} ⋆.

E3.28^{∗} Define the semantics of a universe containing a code for the empty type and a code for the unit type. Show that the set-theoretic model supports such a universe, but that the truth value model does not.

E3.29^{∗} Let Poset be the category of posets and monotone functions. Extend Poset to a CwF by defining Ty(Γ) for poset Γ as the set of down-closed subsets (ideals) of Γ. If σ ∈ Ty(Γ) then define Γ.σ as σ considered as a poset and let p(σ) be the inclusion from σ to Γ. Finally, define Tm(Γ, σ) as [Γ = σ]. For τ ∈ Ty(Γ.σ) let Π′(σ, τ) ∈ Ty(Γ) be {γ∈ Γ | ∀x ∈ σ.x ≤ γ ⇒ x ∈ τ}. Show that Tm(Γ, Π′(σ, τ)) = Tm(Γ.σ, τ), but that nevertheless Π′ does not determine dependent function spaces on Poset because it is not stable under substitution. In fact, the CwF Poset does not support dependent function spaces.

E3.30^{∗} (Extensional type theory) Say that a CwF with identity types supports them in the strict sense if whenever σ ∈ Ty(Γ) and τ ∈ Ty(I(σ)) (recall that I(σ) =^{def} Γ.σ.σ^{+}.Id_{σ}) and H ∈ Tm(τ) then H = R_{σ,τ}^{Id}(H{Refl_{σ}}). Note that this is the case for the CwFs Set and P (Why?). (1) Show that a CwF with identity types supports them in the strict sense iff the morphism Refl_{σ} : Γ.σ → I(σ) is an isomorphism (with inverse Refl_{σ}^{−1} =^{def} (p(σ^{+}))^{+}). (2) Extensional type theory is usually formulated as a type theory with identity types where rules Id-E and Id-C are replaced by the rules

\frac{Γ ⊢ P : Id_{σ}(M, N)}{Γ ⊢ M = N : σ} Reflection  \frac{Γ ⊢ P : Id_{σ}(M, N)}{Γ ⊢ P = Refl_{σ}(M)} Id-Can

Show that the term model of extensional type theory supports identity types in the strict sense. (3) Show that rule Id-Can is independent of Reflection by considering the set-theoretic model with the setting (Id_{σ})_{(γ,x,y)} = {⋆, ⋆′} if x = y and ∅ otherwise. “Independence” is understood informally here; to establish that Id-Can cannot be derived from Reflection one needs the soundness theorem 3.35 below. (4) Show that if a model supports identity types in the strict sense then it supports Σ-types iff it supports them in the strict sense.

3.4 The ω-set model

In this section we present another important CwF which provides a non-trivial interpretation of the Calculus of Constructions in which there is a proposition N̂ ∈ Tm(Prop_{⊤}) such that Tm(Prf (N̂)) has more than one element.

An ω-set X consists of a set (denoted |X| or X) and a relation ⊩_{X}⊆ ω×|X| between natural numbers and elements of X with the property that for each x ∈ |X| there is an n ∈ ω such that n ⊩_{X} x. If n ⊩_{X} x one says that n realises x or codes x or is a code/realiser for x so the condition on ⊩_{X} means that every x ∈ X has a realiser.

A morphism from ω-set X to Y is a function f from X to Y with the property that there exists a partial recursive function e (thought of as a natural number) such that whenever n ⊩_{X} x then {e}(n)—the application of e to n—is defined and realises f(x). The ω-sets together with their morphisms form a category.

An example of an ω-set is N where |N| = ω and n ⊩_{N} m iff n = m. The morphisms in the category of ω-sets from N to N are exactly the total recursive functions. Another example is ⊤ with |⊤| = {⋆} and n ⊩_{⊤} ⋆ for all n ∈ ω. This ω-set is readily seen to be a terminal object. If X is a set then we form an ω-set △X by | △ X| = X and n ⊩_{△X} x for all n ∈ ω and x ∈ X.

The category of ω-sets can be extended to a CwF as follows. For ω-set Γ the set Ty(Γ) consists of families of ω-sets indexed over Γ. Thus, σ ∈ Ty(Γ) means that σ = (σ_{γ})_{γ∈Γ} and each σ_{γ} is an ω-set. A term M ∈ Tm(Γ, σ) is a function assigning to each γ ∈ Γ an element M(γ) ∈ σ_{γ} such that there exists a partial recursive function e with the property that for each γ ∈ Γ and n ⊩_{Γ} γ the computation {e}(n) is defined and {e}(n) ⊩_{σ_{γ}} M(γ).

The ω-set Γ.σ has as underlying set the disjoint union Σ_{γ∈Γ}σ(γ) and n ⊩_{Γ.σ} (γ, x) if L(n) ⊩_{Γ} γ and R(n) ⊩_{σ(γ)} x where L and R are the inverses to a bijection like P (m, n) =^{def} 2^{m}(2n + 1) from ω × ω to ω. The remaining components are left to the reader as an exercise.

The ω-set model supports Π-types with the setting Π(σ, τ)_{γ} = {M ∈ Πx∈ σ_{γ}.τ_{(γ,x)} | ∃e such that T (e, M)} where T (e, M) means that n ⊩_{σ_{γ}} x implies {e}(n) ⊩ M(x) for all x ∈ σ_{γ} and n ∈ ω. If M ∈ Π(σ, τ)_{γ} and e ∈ Γ then e ⊩_{Π(σ,τ)_{γ}} M if T (e, M). Application and abstraction are defined as in the set-theoretic model. The required realisers are obtained from untyped application and abstraction (“smn-theorem”).

All the other type formers we have considered and many more are also supported by the ω-set model.

3.4.1 Modest sets

In an ω-set X two different elements can have the same realiser. An ω-set where this is not so is called a modest set. In other words a modest set consists of a set X and a partial surjective function ⊩_{X} from ω to X. More generally, σ ∈ Ty(Γ) is modest if each σ_{γ} is a modest set. It is easy to see that if τ ∈ Ty(Γ.σ) is modest then so is Π(σ, τ) for arbitrary σ. A modest set X induces a symmetric, transitive relation ∼_{X} (a partial equivalence relation, per) on the set ω of natural numbers by putting m ∼_{X} n if there exists a (necessarily unique) x ∈ X such that m ⊩_{X} x and n ⊩_{X} x. Conversely, if R ⊆ ω×ω is any per we can define a modest set Prf (R) having as underlying set the quotient of {n | nRn} by R (which restricted to this set is an equivalence relation). We have m ⊩_{Prf (R)} [n]_{R} if mRn. If X is modest then X is isomorphic to Prf (∼_{X}) in the category of ω-sets and a per R is equal to ∼_{Prf (R)}. This suggests to interpret the Calculus of Constructions by putting Prop = △(PER) where PER is the set of symmetric and transitive relations on ω. Notice that Prop is not modest. The above-defined operation Prf then yields a type Prf ∈ Ty(Prop). If p : Γ → Prop then p(γ) is a per for each γ ∈ Γ and we have Prf {p}_{γ} = Prf (p(γ)).

If p : Γ.σ → Prop then we define ∀_{σ}(p) : Γ → Prop by (∀_{σ}(p))(γ) =^{def} ∼_{Π(σ,Prf {p})_{γ}}. The verifications are tedious but essentially straightforward.

For mRn iff m = n we have that Prf (R) is isomorphic to the ω-set N which means that we can interpret a type theory in which the impredicative universe Prop contains a code for the natural numbers. Prop also contains codes for other reasonable data types and indeed the ω-sets furnish a model for the CID mentioned in §2.2.3. Beeson (1985) and Allen (1987) show how to model type theory with non-impredicative universes (no ∀) entirely within the pers.

Exercises

E3.31 Let X be any set. Show that every morphism in ω-set from △X to N is constant and that for arbitrary ω-set Y every set-theoretic function from Y to X is a morphism in ω-set from Y to △X.

E3.32 Explain how the set-theoretic model supports lists, cf. E2.3.

E3.33 Explain how the ω-set model supports identity types in the strict sense.

E3.34^{∗} For any ω-set X a per I(X) is defined as the transitive closure of the relation which relates two numbers if they realise a common element of X. Define a morphism η_{X} : X → Prf (I(X)) which sends x ∈ X to the equivalence class of a realiser of x. Show that if Y is a modest set and f : X → Y then there exists a unique morphism f̂: Prf (I(X)) → Y such that f = f̂∘ η_{X}. This means that the modest sets form a reflective sub-category of the ω-sets. One can define impredicative quantification in the ω-set model by ∀_{σ}(M)_{γ∈Γ} =^{def} I(Πx: σ.Prf (M)_{γ}). In (Ehrhard 1989) such a reflection is made part of the definition of a model for the Calculus of Constructions.

3.5 Interpretation of the syntax

We have already implicitly spoken about interpretation of type theory in CwFs by appealing to the informal analogy between components of CwFs and type-theoretic entities. In this section we make this precise by defining an interpretation function and establishing a soundness property.

Assume for the rest of this section a fixed type theory and a CwF C supporting the type and term formers present in this theory. For simplicity we restrict our attention to Π-types.

We define a partial interpretation function [[−]] which maps:

• pre-contexts to objects of C

• pairs Γ ; σ, where Γ is a pre-context and σ is a pre-type, to families in Ty([[Γ]])

• pairs Γ ; M, where Γ is a pre-context and M is a pre-term to elements of Tm(σ) for some σ ∈ Ty([[Γ]]).

The definition is by induction on the lengths of the involved pre-terms, -types, and -contexts. We show below in Thm. 3.35 that the semantic function is defined on all contexts, types, and terms.

The semantic clauses are the following, where we adopt the convention that an expression containing an undefined subexpression is itself undefined. We also adopt the convention that expressions which do not “typecheck”, like Γ.σ if σ ∉ Ty(Γ), are undefined.

• [[⋄]] = ⊤

• [[Γ, x: σ]] = [[Γ]].[[Γ ; σ]] if x not in Γ, undefined otherwise.

• [[Γ ; Πx: σ.τ]] = Π([[Γ ; σ]] , [[Γ, x: σ ; τ]])

• [[Γ, x: σ; x]] = v_{[[Γ; σ]]}

• [[Γ, x: σ, Δ, y: τ ; x]] = [[Γ, x: σ, Δ ; x]]{p([[Γ, x: σ, Δ ; τ]])}

• [[Γ ; App_{[x:σ]τ}(M, N)]] = App_{[[Γ; σ]],[[Γ,x:σ; τ]]} ∘ ⟨\overline{[[Γ ; M]]}, [[Γ ; N]]^{+}⟩_{[[Γ; Πx:σ.τ]]^{+}}

• [[Γ ; λx: σ.M^{τ}]] = λ_{[[Γ; σ]],[[Γ,x:σ; τ]]}([[Γ, x: σ ; M]])

Notice that the semantics of variables is defined by induction on the depth of their declaration as an appropriate weakening of a v_{−}-expression.

Theorem 3.35 The interpretation function enjoys the following soundness properties

• If Γ ⊢ then [[Γ]] is an object of C.

• If Γ ⊢ σ then [[Γ ; σ]] is an element of Ty([[Γ]]).

• If Γ ⊢ M : σ then [[Γ ; M]] is an element of Tm([[Γ ; σ]]).

• If ⊢ Γ = Δ ctxt then [[Γ]] = [[Δ]].

• If Γ ⊢ σ = τ type then [[Γ ; σ]] = [[Γ ; τ]].

• If Γ ⊢ M = N : σ then [[Γ ; M]] = [[Γ ; N]].

The proof of this theorem, although essentially straightforward, presents surprising technical difficulties. The idea is to first establish a substitution lemma which relates syntactic substitution (and weakening) and semantic substitution (−{−}). This is necessary because the equations governing semantic type formers such as Π-C are formulated w.r.t. −{−}, whereas their syntactic counterparts (here Π-C) refer to syntactic substitution which is defined by structural induction. Due to type dependency one needs to account for substitution and weakening in the middle and not merely at the end of a context.

We need some notation first. For pre-contexts Γ, Δ and pre-type ρ we define the expression P(Γ; ρ; Δ) inductively by

P(Γ; ρ; ⋄) = p([[Γ ; ρ]])
P(Γ; ρ; Δ, x: σ) = q(P(Γ; ρ; Δ), [[Γ, Δ ; σ]])

Now let Γ, Δ, ρ be as before and M be a pre-term. We define the expression inductively by the following clauses.

T(Γ; ρ; ⋄; M) = \overline{[[Γ; M]]}
T(Γ; ρ; Δ, x: σ; M) = q(T(Γ; ρ; Δ), [[Γ, z: ρ, Δ ; σ]]) z fresh

The idea is that P(Γ; ρ; Δ) is a morphism from [[Γ, z: ρ, Δ]] to [[Γ, Δ]] projecting out the ρ-part. Similarly, T(Γ; ρ; Δ; M) is intended to go from [[Γ, Δ[M/z]]] to [[Γ, z: ρ, Δ]] yielding [[Γ ; M]] at the z: ρ position and variables otherwise. But that this is really the case has to be proved simultaneously with the weakening and substitution lemmas.

For possibly undefined expressions s, t we write s ≃ t to mean that if either side is defined then so is the other and both agree (Kleene equality).

Lemma 3.36 (Weakening) Let Γ, Δ be pre-contexts, ρ, σ be pre-types, N be a pre-term and z be a fresh variable. Let X ∈ {σ, N}. The expression P(Γ; ρ; Δ) is defined iff [[Γ, z: ρ, Δ]] and [[Γ, Δ]] are defined and in this case is a morphism from the former to the latter. If [[Γ, Δ ; X]] is defined then

[[Γ, z: ρ, Δ ; X]] ≃ [[Γ, Δ ; X]]{P(Γ; ρ; Δ)}

Lemma 3.37 (Substitution) Let Γ, Δ be pre-contexts, ρ, σ be pre-types, M, N be pre-terms, and z a fresh variable. Let X ∈ {σ, N} and suppose that [[Γ ; M]] is defined.

The expression T(Γ; ρ; Δ; M) is defined iff [[Γ, Δ[M/z]]] and [[Γ, z: ρ, Δ]] are both defined and in this case is a morphism from the former to the latter. If [[Γ, z: ρ, Δ ; X]] is defined then

[[Γ, Δ[M/z] ; X]] ≃ [[Γ, z: ρ, Δ]]{T(Γ; ρ; Δ; M)}

The proofs of both lemmas proceed by induction on the lenghts of the involved pre-terms,-types, and -contexts. The most difficult case arises when the term N is a variable. One must then make a case distinction on whether it is declared in Γ or in Δ and perform some equational reasoning. The other cases follow by applying stability under substitution of the participating semantic type and term formers such as Π-S. If the type σ or the term N is a binder like Πx: ϕ.ψ the inductive hypothesis must be used with Δ extended by z: ϕ. In order to prove the correct typing of the P and T morphisms one uses the second part of each lemma with shortened Δ.

After this introduction we leave the proofs themselves to the reader as following the calculations seems to require as much effort as doing them by oneself.

Given the above two lemmas the proof of the soundness theorem becomes a straightforward induction on derivations. For the same reason as before this proof will not be reproduced here; the reader is instead encouraged to carry out at least a few cases of the inductive argument by himself and in case of serious difficulty consult Streicher’s monograph (1991) where the verification of the corresponding interpretation in contextual categories is spelt out in a very detailed fashion.

The method of partially interpreting pre-syntax first and proving definedness by induction on derivations was invented by Streicher (1991) and is used in order to ensure that the interpretation does not depend on the particular derivation chosen. Notice that derivations of a given judgement are not unique as instances of the conversion rules Ty-Conv and Tm-Conv are not recorded in judgements. Alternatively, one could define the interpretation by induction on derivations and then use the device of pre-syntax to establish coherence of the semantics with respect to the conversion rules, but this would result in a more complicated proof. For a particular model this has been carried out in (Palmgren and Stoltenberg-Hansen 1990).

Exercises

E3.38 Extend the interpretation function to Σ-types

E3.39^{∗} Formulate a completeness theorem for the semantics and use the term model to prove it. Deduce from the term model that if Γ ⊢ M : σ and Γ ⊢ M : τ then Γ ⊢ σ = τ type.

E3.40 Explain why the interpretation function cannot be defined in the same way as we did in case application is not typed, i.e., with App_{[x:σ]τ}(M, N) replaced by (M N). Also explain why it would not matter to leave out the type annotation τ in λx: σ.M^{τ} and similar situations.

E3.41 Try to define the interpretation function on triples Γ ; M ; σ of typed terms in context rather than on the pairs Γ ; M. What goes wrong?

E3.42^{∗} Extend the interpretation function to syntactic context morphisms and state a general substitution lemma for context morphisms (Pitts 1997). It seems difficult to prove this general substitution lemma directly without using Lemmas 3.36 & 3.37.

E3.43 Deduce from E3.26 and the soundness theorem that the following type is not inhabited in a type theory without universes.

⋄ ⊢ Id_{N}(0, Suc(0)) → 0 type

E3.44 Use the ω-set model to derive that in the Calculus of Constructions with natural numbers there does not exist a term ⋄ ⊢ M : Prop → N and propositions ⋄ ⊢ P : Prop and ⋄ ⊢ Q : Prop such that ⋄ ⊢ App(M, P) = 0 : N and ⋄ ⊢ App(M, Q) = Suc(0) : N

E3.45^{∗} Show that the interpretation of existential quantification ∃x: σ.P as defined in E2.8 in the set-theoretic model is tt if P (x) is tt for some x ∈ [[σ]] and ff otherwise. Conclude that the following extension of the Calculus of Constructions by a choice function is consistent in the sense that neither the empty type (if it exists) nor the type Prf (∀c: Prop.c) is inhabited in the empty context:

\frac{Γ ⊢ H : Prf (∃x: σ.P)}{Γ ⊢ Choice(H) : σ}

It is known that such choice function becomes inconsistent if in addition one imposes the equation

⊢ Choice(∃-I(M, N)) = M : σ

for all M: σ and N: Prf (P [M]), see (Coquand 1990).

4 Extended example: presheaf models

In this section we encounter a family of interpretations of type theory which generalises the set-theoretic model in that types are interpreted as variable sets (presheaves) or families of such. There are various applications of such interpretations, see for example (Asperti and Martini 1992) and (Altenkirch, Hofmann, and Streicher 1996) where they are used to define models of the polymorphic lambda calculus in which type quantification is interpreted as cartesian product. We use a presheaf interpretation here to show that the Logical Framework in the sense of §2.2.2 forms a conservative extension of ordinary type theory. This result appears here for the first time; a more detailed version will be published elsewhere.

Preliminaries. Let K be a (small) category. A presheaf over K is a contravariant functor from K to the category Set of sets and functions. We denote by K̂ the functor category Set^{K^{op}} of presheaves over K. We denote presheaf application by subscripting. That is, if F ∈ K̂ and u ∈ K(I, J) then F_{u} : F_{J} → F_{I}. If μ ∈ K̂(F, G) then μ_{I} : F_{I} → G_{I}. We may think of K as a category of stages or worlds and of a presheaf as a set varying with these stages. The Yoneda embedding y : K → K̂ sending I to K(−, I) is a full and faithful embedding of the stages into K̂. See (Barr and Wells 1990) for more information on presheaves.

4.1 Presheaves as a CwF

Our aim is to construct a CwF which has K̂ as the category of contexts. This category has a terminal object given by ⊤_{I} = {⋆}. We define types, substitution, terms, and comprehension in order. From now on we will use the generic letters Γ, f, σ, … to range over presheaves, natural transformations, families of presheaves, etc. if these arise in the context of a CwF.

If Γ is a presheaf then we form its category of elements ∫ (Γ) with objects (I, γ) where I ∈ K and γ ∈ Γ_{I}. A morphism from (J, γ′) to (I, γ) is a Kmorphism u ∈ K(J, I) such that Γ_{u}(γ) = γ′. In other words, if u ∈ K(J, I) and γ ∈ Γ_{I} then u is an ∫ (Γ)-morphism from (J, Γ_{u}(γ)) to (I, γ). If appropriate we may also write (u, γ) for this morphism. Composition is inherited from K.

For presheaf Γ ∈ K̂ we define the set Ty(Γ) to consist of the presheaves over ∫ (Γ). If σ ∈ Ty(Γ) and (I, γ) ∈ ∫ (Γ) then we write σ_{I}(γ) rather than σ_{(I,γ)} for σ at argument (I, γ) and similarly for morphisms. That σ is a presheaf means that if u ∈ K(J, I) and γ ∈ Γ_{I} and x ∈ σ_{I}(γ) then σ_{u}(γ)(x) ∈ σ_{J}(Γ_{u}(γ)) and this action is compatible with composition and identities in K.

Now suppose that f : Δ → Γ is a natural transformation. We define a functor ∫ (f) : ∫ (Δ) → ∫ (Γ) by ∫ (f)(I, δ) = (I, f_{I}(δ)) and for u ∈ K(J, I), δ ∈ Δ_{I} we define ∫ (f)(u, δ) = (u, f_{I}(δ)). Now if σ ∈ Ty(Γ) is a family of presheaves then we define σ{f} ∈ Ty(Δ) as the composition σ ∘ ∫ (f). So, we have σ{f}_{I}(δ) = σ_{I}(f_{I}(δ)). It is clear that this has the required functoriality properties.

Next we define terms. If σ ∈ Ty(Γ) then an element M of Tm(σ) assigns to each stage I and element γ ∈ Γ_{I} an element M_{I}(γ) ∈ σ_{I}(γ) in such a way that if u ∈ K(J, I) then σ_{u}(γ)(M_{I}(γ)) = M_{J}(Γ_{u}(γ)). If M ∈ Tm(σ) and f : Δ → Γ then M{f} ∈ Tm(σ{f}) is given by composition as M{f}_{I}(δ) = M_{I}(f_{I}(δ)).

If σ ∈ Ty(Γ) then the presheaf Γ.σ is defined by (Γ.σ)_{I} = {(γ, x) | γ∈ Γ_{I} , x∈ σ_{I}(γ)}. If u ∈ K(J, I) and (γ, x) ∈ (Γ.σ)_{I} then (Γ.σ)_{u}(γ, x) = (Γ_{u}(γ), σ_{u}(γ)(x)). The projection p(σ) is defined by p(σ)_{I}(γ, x) = γ; the variable v_{σ} ∈ Tm(σ{p(σ)}) is defined by (v_{σ})_{I}(γ, x) = x. Finally, if f : Δ → Γ and M ∈ Tm(σ{f}) then (⟨f, M⟩_{σ})_{I}(δ) = (f_{I}(δ), M_{I}(δ)). The verifications are straightforward expansions of the definitions. We have thus established that presheaves over K furnish a CwF.

4.2 Type formers in K̂

The presheaf model supports most of the type formers the set-theoretic model supports, often by the very same constructions. The major difference is the interpretation of Π-types which is carried out in a way similar to the treatment of implication in Kripke models, and of course similar to the definition of exponentiation in functor categories.. Suppose that σ ∈ Ty(Γ) and τ ∈ Ty(Γ.σ). Following the convention from §2.2.2 we will write (σ)τ rather than Π(σ, τ) for the dependent function space of σ and τ. It is defined as follows. If I ∈ K and γ ∈ Γ_{I} then an element f of (σ)τ_{I}(γ) associates to J ∈ K and w : J → I and x ∈ σ_{J}(Γ_{w}(γ)) an element f(w, x) ∈ τ_{J}(Γ_{w}(γ), σ_{w}(γ)(x)). Notice that w ∈ ∫ (Γ)((J, Γ_{w}(γ)) , (I, γ)) and thus σ_{w}(γ)(x) ∈ σ_{I}(Γ_{w}(γ)). Moreover the assignment f must be natural in the sense that if in addition w′ : J′ → J then

f(w ∘ w′, σ_{w′}(Γ_{w}(γ))(x)) = τ_{w′}(Γ_{w}(γ), σ_{w}(γ)(x))(f(w, x))

The generalisation to “later stages” J is necessary to make (σ)τ a presheaf and not merely an assignment of sets to stages. Indeed, if v : I′ → I and f ∈ (σ)τ_{I}(γ) then we can define (σ)τ_{v}(Γ_{v}(γ))(f) ∈ (σ)τ′_{I}(Γ_{v}(γ)) by

(σ)τ_{v}(Γ_{v}(γ))(f)(w: J → I′, x∈ σ_{J}(Γ_{w}(Γ_{v}(γ)))) =^{def} f(v ∘ w, x)

which is valid because Γ_{w}(Γ_{v}(γ)) = Γ_{v∘w}(γ).

If M ∈ Tm(Γ.σ, τ) then λ_{σ,τ}(M) ∈ Tm((σ)τ) is given by

λ(M)_{I}(γ∈ Γ_{I} , J∈ K, w : J → I, x∈ σ_{J}(Γ_{w}(γ))) =^{def} M_{J}(Γ_{w}(γ), x)

The application morphism App_{σ,τ} : Γ.σ.(σ)τ^{+} → Γ.σ.τ maps at stage I elements γ ∈ Γ_{I} and x ∈ σ_{I}(γ) and f ∈ (σ)τ_{I}(γ) to f(id_{I}, x) ∈ τ_{I}(γ, x). It is routine to check that this defines dependent function spaces in the strict sense.

The dependent sum Σ(σ, τ) of the presheaves above is given by stage-wise set-theoretic dependent sum. This means that

Σ(σ, τ)_{I}(γ) = {(x, y) | x∈ σ_{I}(γ) ∧ y∈ τ_{I}(γ, x)}

We omit the associated term formers. We remark without proof that K̂ supports natural numbers and other inductive types; it also supports universes if the ambient set theory w.r.t. which the presheaves are formed supports them.

4.3 Conservativity of the logical framework

Let T be a theory of dependent types like one of those set out in §2. The precise nature of T is unimportant.

Furthermore, we let T_{LF} denote the Logical Framework presentation of T , i.e., a dependent type theory with Π-types and one universe Set together with constants and equations corresponding to the type and term formers in T . We have a conversion map i translating terms, types, and judgements in T into ones in T_{LF} in such a way that judgements are preserved. More precisely, if Γ ⊢ J in T then i(Γ) ⊢ i(J) in T_{LF}. For distinction, we write ⊢_{T} and ⊢_{T_{LF}} for the judgement relations in the two type theories. For example, in T we might have

x: N ⊢_{T} Πy: N.Id(x, y) → Id(y, x) type

Applying the translation yields the following judgement in T_{LF}:

x: El(N̂) ⊢_{T_{LF}} El(Π̂y: El(N̂).Îd(x, y) ˆ→Îd(y, x)) type

In other words, i(N) = El(N̂), etc. If we omit the El-operator and the ˆ−- decorations then the translated judgement looks exactly like the one to start with. We will do so in the sequel and omit the coercion i.

Due to the presence of type variables T_{LF} is a proper extension of T . Judgements like ⊢ Set type or F: N → Set ⊢ F (0) are not in the image of i. A natural question to ask is whether T_{LF} is conservative over T . There is more than one way to extend the notion of conservativity from logic to theories of dependent types. We will here use the simplest one and prove the following theorem:

Theorem 4.1 If Γ ⊢_{T} σ type and Γ ⊢_{T_{LF}} M : σ for some term M then there exists a term M′ such that Γ ⊢_{T} M′ : σ.

Notice that M itself need not be a legal T -term, it could for instance contain a subterm like ([X: Set]Suc(0))(N) which is equal, but not identical to Suc(0).

Our strategy for proving this theorem consists of exhibiting a model of T_{LF} with the property that the interpretation of T in it (notice that such a model also models T ) is full. That is to say, if Tm([[Γ ; σ]]) ≠ ∅ for some Γ ⊢_{T} σ type then there exists M with Γ ⊢_{T} M : σ. Such a model is furnished by the presheaf model T̂ where T is the (category of contexts of the) term model of T . The fullness of the interpretation of T in T̂ is essentially a consequence of the Yoneda lemma and will be proved at the end of this section.

Let us first show how T̂ models the Logical Framework. We have already demonstrated that T̂ (like every presheaf model) supports dependent function spaces. We interpret Set ∈ Ty T̂(⊤) ≅ T̂ as the presheaf Ty_{T} which to a context Γ ∈ T associates the T -types in context Γ quotiented by definitional equality. The interpretation of El ∈ Ty T̂(⊤.Set) ≡ ; ∫ (Set) is defined as the presheaf Tm_{T} which to Γ ∈ |T | and σ ∈ Ty_{T} (Γ) = Set_{Γ} associates the set Tm_{T} (Γ, σ) of terms of type σ in context Γ factored by definitional equality. This extends to a presheaf by term substitution.

For the demonstration that T̂ models T_{LF} it remains to show that Set contains codes for all the type and term formers present in T . We will deal with this task by way of example and assume that T contains Π-types and the (ad hoc) operator L from §2.2.2.

We deal with the L-operator first. In order to simplify the notation and in view of the soundness and completeness of the semantics we will use the syntax of type theory with named variables to denote entities in T̂. Thus we require an element L̂ ∈ Tm(⊤, (Set)Set) and an element l̂ ∈ Tm(⊤, (σ: Set, m: El(σ))El(L(σ))). Since the dependent function spaces in T̂ are strict the first task is equivalent to exhibiting an element, for simplicity also denoted L̂, of TmT̂(σ: Set , Set) which we describe explicitly by

L̂_{Γ}(σ ∈ Ty_{T} (Γ)) =^{def} L(σ)

Recall that Set_{Γ} = Ty_{T} (Γ). The naturality of this assignment amounts to checking that for f : B → Γ and σ ∈ Ty_{T} (Γ) we have L(σ)[f] = L(σ[f]) which is immediate from the properties of syntactic substitution.

Similarly, the second task is equivalent to finding a term

l̂ ∈ TmT̂(σ: Set, M: El(σ) , El(L̂(σ)))

Again, we define it explicitly by

l̂_{Γ}(σ∈ Ty_{T} (Γ), M∈ Tm_{T} (Γ, σ)) = l(M) ∈ Tm_{T} (Γ, σ)

Recall here that El_{Γ}(σ) = Tm_{T} (Γ, σ). Naturality is again a consequence of stability under substitution. Notice that up to the necessary abstraction e.g. from Tm(σ: Set , Set) to Tm((Set)Set) the required constants in K̂ are given exactly by their counterparts in T .

In essence, this is also the case for the Π-type, but due to the binding behaviour we encounter a slight complication. We wish to construct an element of

TmT̂(⊤, (σ: Set, τ: (El(σ))Set)Set)

By “uncurrying” this amounts to constructing a term Π̂ of

TmT̂(σ: Set, τ: (El(σ))Set , Set)

At stage Γ the arguments to Π̂ are a type σ ∈ Ty_{T} (Γ) and an element of (El(σ))Set_{Γ}. Call the latter set X temporarily. An element τ of X associates by definition of dependent function spaces in K̂ to f : B → Γ and M ∈ Tm_{T} (B, σ{f}) a type τ(B, f, M) ∈ Ty(B). This assignment is natural in the sense that for f′ : B′ → B we have τ(B′, f ∘ f′, M{f′}) = τ(B, f, M){f′} ∈ Ty(B′). But this means that the whole of τ can be reconstructed from its particular instance τ_{0} =^{def} τ(Γ.σ, p(σ), v_{σ}) ∈ Ty(Γ.σ). Indeed, for arbitrary f : B → Γ and M ∈ Ty(σ{f} we have that τ(B, f, M) = τ_{0}{⟨f, M⟩_{σ}} by naturality and equations (Cons-L) and (Cons-R). By (Cons-Id) we also get the converse and have thus established a bijective correspondence between the sets (El(σ))Set_{Γ} and Ty_{T} (Γ.σ = Set_{Γ.σ}. Therefore, the arguments at stage Γ to the term Π̂ which we aim to construct amount to a type σ ∈ Ty(Γ) and a type τ_{0} ∈ Ty(Γ.σ). We define the result as the syntactic dependent function space Π(σ, τ_{0}) in T . Summing up, we have defined

Π_{Γ}(σ∈ Set_{Γ}, τ∈ (El(σ))Set) = Π_{T} (σ, τ(Γ.σ, p(σ), v_{σ}))

So up to the bijection between the function space (El(σ))Set_{Γ} and the set of types in Γ.σ the Π-constant in T_{LF} has again been obtained directly from its syntactic companion. The same goes for the other constants λ̂ and Âpp whose definition we omit. In the case of λ̂ we face again an argument of the dependent function space type (x: El(σ))El(τ) which at stage Γ is isomorphic to Tm_{T} (Γ.σ , τ) by an analysis similar to the one which led to the characterisation of (El(σ))Set before.

One can more generally characterise the dependent function spaces of the form (El(−))F for arbitrary presheaf F as certain “shifts” of F. This allows for a systematic translation of arbitrary type and term formers possibly binding variables from T to T_{LF}. The general strategy should have become clear from the example of Π. The important point is that in K̂ the function space (El(σ))Set is so strongly confined by the naturality condition that it only contains functions induced by a syntactic type with free variable of type σ.

Proof of Thm. 4.1 Suppose that Γ ⊢_{T} σ type and that Γ ⊢_{T_{LF}} M : σ. By induction on derivations we find that the interpretations of Γ and σ in T̂ have the following properties:

[[Γ]]_{Δ} ≅ T (Δ, Γ)

and

[[Γ ; σ]]_{Δ}(f ∈ T (Δ, Γ)) = σ[f] ∈ Set_{Δ}

Thus, in particular, we have [[Γ ; σ]]_{Γ}(id_{Γ}) = σ. Therefore, the interpretation of M in T̂ yields [[Γ ; M]]_{Γ}(id_{Γ}) ∈ Tm_{T} (Γ, σ); thus Γ ⊢_{T} M′ : σ for any representative M′ in the class [[Γ ; M]]. The theorem is proved. □

One may consider a Logical Framework which does not only support Πtypes, but several other type formers like Σ-types, e.g. for modularisation and natural numbers, e.g. to define syntax. As long as these type formers are supported by T̂ (Σ and N are) the conservativity theorem continues to hold by the same proof. Using a dependent version of the glueing construction (Crole 1993) it is possible to obtain the stronger property that the term M′ in Thm. 4.1 is T_{LF}-equal to M.

We also remark that we have not used any particular properties of the term model in the construction of the presheaf model so that it can be formed out of any CwF and thus gives a canonical way to lift a model of some type theory to a model for the presentation of this type theory in the Logical Framework.

5 Other applications of semantic methods

We give some directions for further reading on the subject of semantical methods in the study of theories of dependent types. Independence results are the subject of (Streicher 1992) and (Hofmann and Streicher 1994). Semantical methods in order to derive syntactic properties of type theories like strong normalisation and thus decidability of type checking have been used in (Hyland and Ong 1993; Altenkirch 1994; Goguen 1995). In (Moggi 1991) and (Harper, Mitchell, and Moggi 1990) categories with attributes are used to give an account of higher-order modules in functional programming. There is an intriguing connection with Paulin’s work on program extraction in type theory (Paulin-Mohring 1989) and the “deliverables” approach to program development (Burstall and McKinna 1993). In each of these works a type is modelled as a type or a set together with a predicate or a dependent type and terms are modelled as terms which preserve these predicates. A similar interpretation has been used in (Hofmann 1995a) where a translation of a type theory with a quotient type former into ordinary type theory and other applications of syntactic models are described.

Connections between category-theoretic semantics and abstract machines have been noticed in (Curien 1986) and (Ehrhard 1988) and were subsequently exploited and applied in (Ritter 1992) where an evaluator for the Calculus of Constructions is derived from its category-theoretic semantics.

Last, but not least we mention the use of domain-theoretic interpretations of type theory in order to establish the consistency of general recursion and fixpoint combinators with dependent types (Palmgren and Stoltenberg-Hansen 1990). In a similar direction goes (Reus 1995) where an interpretation of type theory using synthetic domain theory has been employed to establish the consistency of a very powerful dependent type theory incorporating higher-order logic, general recursion, and impredicativity.

References

Allen, S. (1987). A non-type-theoretic account of Martin-Löf’s types. In Symposium on Logic in Computer Science.

Altenkirch, T. (1994). Proving strong normalization of CC by modifying realizability semantics. In H. Barendregt and T. Nipkow (Eds.), Types for Proofs and Programs, Springer LNCS Vol. 806, pp. 3–18.

Altenkirch, T., M. Hofmann, and T. Streicher (1996). Reduction-free normalisation for a polymorphic system. In Proc. of the 11th IEEE Symp. on Logic in Comp. Sci. (LICS), New Brunswick, New Jersey.

Asperti, A. and S. Martini (1992). Categorical models of polymorphism. Information and Computation 99, 1–79.

Barr, M. and C. Wells (1990). Category Theory for Computing Science. International Series in Computer Science. Prentice Hall.

Beeson, M. (1985). Foundations of Constructive Mathematics. Springer.

Burstall, R. and J. McKinna (1993). Deliverables: An approach to program semantics in constructions. In Proc. MFCS ’93, Springer LNCS, Vol.

711. Also as LFCS technical report ECS-LFCS-91-133.

Cartmell, J. (1978). Generalized Algebraic Theories and Contextual Categories. Ph. D. thesis, Univ. Oxford.

Constable, R. et al. (1986). Implementing Mathematics with the Nuprl Development System. Prentice-Hall.

Coquand, T. (1990). Metamathematical investigations of a calculus of constructions. In P. Odifreddi (Ed.), Logic and Computer Science, pp. 91– 118. Academic Press Ltd.

Coquand, T. and G. Huet (1988). The Calculus of Constructions. Information and Computation 76, 95–120.

Coquand, T. and C. Paulin-Mohring (1989). Inductively defined types. In LNCS 389. Springer.

Crole, R. (1993). Categories for Types. Cambridge University Press.

Curien, P.-L. (1986). Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman.

Curien, P.-L. (1989). Alpha-conversion, conditions on variables and categorical logic. Studia Logica 3, 318–360.

Curien, P.-L. (1993). Substitution up to isomorphism. Fundamenta Informaticae 19, 51–86.

Dowek, G. et al. (1991, Dec.). The COQ proof assistant user’s guide, V5.6. Rapport technique 134, INRIA Rocquencourt.

Dybjer, P. (1996). Internal type theory. In Proc. BRA TYPES workshop, Torino, June 1995, Springer LNCS. To appear.

Ehrhard, T. (1988). Une sémantique catégorique des types dépendants. Application au Calcul des Constructions. Ph. D. thesis, Univ. Paris VII.

Ehrhard, T. (1989). Dictoses. In Proc. Conf. Category Theory and Computer Science, Manchester, UK, pp. 213–223. Springer LNCS Vol. 389.

Goguen, H. (1995). Typed operational semantics. In Proc. TLCA ’95, Edinburgh, Springer LNCS Vol. 902.

Harper, R., F. Honsell, and G. Plotkin (1993, January). A framework for defining logics. Journal of the ACM 40(1), 143–184.

Harper, R. and J. C. Mitchell (1993). On the type structure of Standard ML. ACM Trans. Programming Lang. and Systems 15(2), 211–252.

Harper, R., J. C. Mitchell, and E. Moggi (1990). Higher-order modules and the phase distinction. In Conference record of the 17th ACM Symposium on Principles of Programming Languages (POPL), San Francisco, CA USA, pp. 341–354.

Hofmann, M. (1995a). Extensional Concepts in Intensional Type Theory. Ph. D. thesis, Univ. of Edinburgh.

Hofmann, M. (1995b). On the interpretation of type theory in locally cartesian closed categories. In J. Tiuryn and L. Pacholski (Eds.), Proc. CSL ’94, Kazimierz, Poland, Springer LNCS, Vol. 933, pp. 427–442.

Hofmann, M. (1996). Conservativity of equality reflection over intensional type theory. In Proc. BRA TYPES workshop, Torino, June 1995, Springer LNCS. To appear.

Hofmann, M. and T. Streicher (1994). A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris.

Huet, G. (1990). A uniform approach to type theory. In Logical Foundations of Functional Programming. Addison-Wesley.

Hyland, J. M. E. and C.-H. L. Ong (1993). Modified realisability toposes and strong normalisation proofs. In J. F. Groote and M. Bezem (Eds.), Typed Lambda Calculi and Applications, Springer LNCS, Vol. 664.

Hyland, M. and A. Pitts (1989). The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models. In Categories in Computer Science and Logic. AMS.

Jacobs, B. (1991). Categorical Type Theory. Ph. D. thesis, University of Nijmegen.

Jacobs, B. (1993). Comprehension categories and the semantics of type theory. Theoretical Computer Science 107, 169–207.

Lamarche, F. (1987). A simple model for the theory of constructions. In J. W. Gray and A. Scedrov (Eds.), Proc. of AMS Research Conf., Boulder, Colorado, pp. 137–199. AMS.

Lambek, J. and P. Scott (1985). Introduction to Higher-Order Categorical Logic. Cambridge University Press.

Luo, Z. (1991). Program specification and data refinement in type theory. In S. Abramsky and T. S. E. Maibaum (Eds.), Proc. TAPSOFT ’91, Springer LNCS, Vol. 493, pp. 142–168.

Luo, Z. (1994). Computation and Reasoning. Oxford University Press.

Luo, Z. and R. Pollack (1992). LEGO Proof Development System: User’s Manual. Technical Report ECS-LFCS-92-211, University of Edinburgh.

Magnusson, L. and B. Nordström (1994). The ALF proof editor and its proof engine. In H. Barendregt and T. Nipkow (Eds.), Types for Proofs and Programs, Springer LNCS Vol. 806, pp. 213–237. Springer-Verlag.

Martin-Löf, P. (1975). An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Sheperdson (Eds.), Logic Colloquium 1973, pp. 73–118. North-Holland.

Martin-Löf, P. (1982). Constructive mathematics and computer programming. In Proceedings of the Sixth International Congress for Logic, Methodology and Philosophy of Science, pp. 153–175.

Martin-Löf, P. (1984). Intuitionistic Type Theory. Bibliopolis·Napoli.

Moggi, E. (1991). A category-theoretic account of program modules. Math. Struct. in Comp. Sci. 1(1), 103–139.

Nordström, B., K. Petersson, and J. M. Smith (1990). Programming in Martin-Löf’s Type Theory, An Introduction. Clarendon Press, Oxford.

Obtułowicz, A. (1989). Categorical and algebraic aspects of Martin-Löf type theory. Studia Logica 3, 299–317.

Palmgren, E. and V. Stoltenberg-Hansen (1990). Domain interpretation of Martin-Löf’s partial type theory. Ann. of Pure and Appl. Logic 48, 135–196.

Paulin-Mohring, C. (1989). Extracting F_{ω}’s programs from proofs in the calculus of constructions. In Principles of Programming Languages (POPL), pp. 1–17. ACM.

Pitts, A. (1997). Categorical logic. In Handbook of Logic in Computer Science (Vol. VI). Oxford University Press. To appear.

Reus, B. (1995). Program verification in Synthetic Domain Theory. Ph. D. thesis, LMU, München.

Reynolds, J. C. and G. D. Plotkin (1988, May). On functors expressible in the polymorphic typed lambda calculus. Technical Report ECS-LFCS-88-53, University of Edinburgh.

Ritter, E. (1992). Categorical Abstract Machines for Higher-Order Typed Lambda Calculi. Ph. D. thesis, University of Cambridge.

Seely, R. A. G. (1984). Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society 95, 33–48.

Smith, J. (1988). The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. Journal of Symbolic Logic 53(3).

Streicher, T. (1991). Semantics of Type Theory. Birkhäuser.

Streicher, T. (1992). Dependence and independence results for (impredicative) calculi of dependent types. Math. Struct. Comp. Sci. 2, 29–54.

Streicher, T. (1993). Semantical Investigations into Intensional Type Theory. Habilitationsschrift, LMU München.

Taylor, P. (1986). Recursive Domains, Indexed Category Theory, and Polymorphism. Ph. D. thesis, University of Cambridge.

Troelstra, A. and D. van Dalen (1988). Constructivism in Mathematics, An Introduction, Volume I. North-Holland.