Reduction-free normalisation for system F

Thorsten Altenkirch

Institut für Informatik,LMU-München Oettingenstr. 67 D-80538 München Germany

e-mail:alti@informatik.uni-muenchen.de

Martin Hofmann and Thomas Streicher

TH Darmstadt, FB 4, Schloßgartenstr. 7, 64289 Darmstadt, Germany

e-mail:{mh|streicher}@mathematik.th-darmstadt.de July 2, 1996

Running title:

Reduction-free normalisation for system F

Address for correspondence:

Martin Hofmann TH Darmstadt, FB 4 Schloßgartenstr. 7 64289 Darmstadt, Germany e-mail:mh@mathematik.th-darmstadt.de

Abstract

We present a semantical proof of existence of normal forms for system F including η-equality. A reduction-free normalisation function can be obtained from this. The proof uses the method of glueing (a variant of) the term model along the global sections functor, carried out in the internal language of a category of presheaves. As a by-product we obtain an semantical explanation of higherorder abstract syntax. The paper extends a previous one (Altenkirch, Hofmann, and Streicher 1996) in which a combinatory version of system F has been treated.

1 Introduction

In this paper we give a semantical proof of reduction-free normalisation for F_{βη}, a version of Girard’s system F with full βη-equality for both kinds of abstraction. This generalises the semantical normalisation algorithms for simply-typed systems (Berger and Schwichtenberg 1991; Coquand and Dybjer 1996; Altenkirch, Hofmann, and Streicher 1995) to polymorphism.

As in those approaches we do not prove strong normalisation but construct a function nf sending terms to terms in normal form such that convertible terms are sent to the same normal form and any term t is convertible with nf (t). Such a function is sufficient for practical purposes as it allows one for every term to compute a normal form and consequently to decide equality of terms. These “normal forms” are computed by structural induction; no notion of term rewriting whatsoever is used although the normal forms computed by our algorithm are also normal forms in the sense of term rewriting, more precisely, they are long βη-normal forms in the sense of e.g. (Huet 1976)

This work is part of a larger programme aiming at deriving reduction-free normalisation algorithms for more complex systems such as Martin-Löf type theory, Extended Calculus of Constructions (ECC), and variants of the Logical Framework. The ultimate goal would be to derive implementations of these systems which would be more efficient than the existing ones because the reduction-free normalisation algorithms can employ the interpreter of the underlying functional programming language as e.g. Standard ML. This gain of efficiency was the initial motivation of Berger and Schwichtenberg for studying reduction-free normalisation.

The case of simply-typed lambda calculus has been treated by the abovementioned authors. The richer systems like ECC extend the simply-typed lambda calculus by two new features: type dependency and polymorphism. We treat the latter in this paper and leave type dependency for future work.

The key idea of the present work (and also implicit in (Coquand and Dybjer 1996)) is to construct a model GT (for Girard-Tait or Glueing of the Term model) in which types are interpreted as quadruples (A, A^{pred}, q^{A}, u^{A}) where A is a syntactic type, A^{pred} is a family of “sets” indexed by conversion classes of terms of A, q^{A} (“quote”) is a function mapping an element of A^{pred}([t]) to a normal form in [t], i.e. convertible with t, and finally u^{A} (“unquote”) is a function mapping a neutral term t, i.e. a variable applied to normal forms, to an element of the set A^{pred}([t]). Unlike in (Coquand and Dybjer 1996), where these “sets” are ordinary sets, in our model they are replaced by presheaves over the finite-product category 𝕍 of types and variable renamings which has as objects pairs [n, Γ] where Γ is a F_{βη}-context in n free type variables. A 𝕍-morphism from [n, Γ] to [m, Δ] is an m-tuple A⃗ of types in n free type variables together with a renaming w from Γ to Δ[A⃗].

We summarise our main technical results. Our constructions are carried out within (models of) an impredicative Type Theory, i.e. an extensional version of the Calculus of Constructions extended by inductive types (e.g. similar to (Luo 1994)). We prove that the category 𝕍̂ of presheaves over 𝕍 with values in the constructive sets of our metalanguage forms itself a model of impredicative type theory. Generalising a result in (Asperti and Martini 1992) we construct a term model of F_{βη} living inside 𝕍̂ in which type quantification becomes “set-theoretic” dependent product (inside 𝕍̂). Furthermore, we show that in the term model there exists a higher-order abstraction operation which constructs a term of type A ⇒ B from a 𝕍̂-function mapping variables of type A to terms of type B. In this way our term model can be seen as a model for higher-order abstract syntax in the sense of (Despeyroux, Felty, and Hirschowitz 1995).

The main result consists of the construction of the glued model GT now internal to the category Fam(𝕍̂) of families or deliverables in 𝕍̂. The objects of GT can be considered as a naive version of Tait’s computability predicates. Morphisms are maps respecting these. The desired result on reduction-free normalisation is an immediate corollary of the correctness of this model.

Our approach is modular in the sense that we first identify a collection of objects and functions in 𝕍̂ together with equations satisfied by those and then construct the model GT entirely within the internal language of 𝕍̂, i.e. using impredicative type theory augmented by these objects and functions (and the equations). Apart from simplifying the exposition this makes it possible to use an implementation of impredicative type theory, for instance Lego (Luo and Pollack 1992) to define the model GT and to prove its correctness. In our previous paper (Altenkirch, Hofmann, and Streicher 1995) we were not yet able to formulate the glued model entirely within the internal language resulting in more complicated definitions and proofs. The methods developed in this paper apply just as well to the simply-typed case dealt with in loc. cit. and would result in a considerable simplification.

We assume some knowledge of category theory and in particular a certain acquaintance with categories of presheaves. A type-theoretically skilled reader who does not have this background may still take profit of our paper by taking the context of definitions summarised in Fig. 8.3 for granted and going through the construction of the model GT on top of this context.

2 Syntax

The system F_{βη} is a variant of Girard’s System F with full βη-equality. We use de Bruijn indices to represent variables; the judgement n ⊢ A means that A is a type with at most n free variables and is defined as follows :

\frac{i < n}{n ⊢ i} (Var)  \frac{n ⊢ A  n ⊢ B}{n ⊢ A ⇒ B} (⇒)  \frac{n + 1 ⊢ A}{n ⊢ ∀(A)} (∀)

We define the category 𝕊 of type substitutions : objects are natural numbers and a morphism in 𝕊(m, n) is an n-tuple of types A⃗ = (A_{n−1}, … A_{0}) where m ⊢ A_{i} for i = 0, … n − 1. Notice the right to left decomposition of such tuples, i.e. the “first” element of A⃗ is A_{0}, its leftmost entry.

Composition is given by substitution which can be defined as a recursive function over the syntax. 𝕊 has a terminal object 0 and finite products which are given on objects by addition of natural numbers. Here and in the sequel we use the standard notation π, π′, ⟨−, −⟩ for projections and pairing possible decorated with typing subscripts. We write ⟨⟩ for the unique morphism into a terminal object.

If n + 1 ⊢ A and n ⊢ B then we write A[B] for A ∘⟨id_{n}, B⟩ and B^{+} for B ∘ π_{n,1}. We have n ⊢ A[B] and n + 1 ⊢ B^{+}.

Given a natural number n, a context n ⊢ Γ is a sequence of types in n variables, i.e. of types A such that n ⊢ A. We denote the length of a context by |Γ| and decompose Γ as Γ = (Γ_{|Γ|−1}, … Γ_{0}). Note that a context n ⊢ Γ is an 𝕊-morphism from n to |Γ|. We write ⋄ for the empty context and Γ.A for the extension of context Γ by type A. The operation Γ^{+} arises as the pointwise extension of A^{+}. We define a judgement Γ ⊢_{n} t : A, where n ⊢ Γ and n ⊢ A by the following rules:

\frac{i < |Γ|}{Γ ⊢_{n} i_{Γ} : Γ_{i}} (tm-var)
\frac{Γ.A ⊢_{n} t : B}{Γ ⊢_{n} λ_{Γ,A,B}(t) : A → B} (λ)  \frac{Γ ⊢_{n} t : A → B  Γ ⊢_{n} s : A}{Γ ⊢_{n} app_{Γ,A,B}(t, s) : B} (app)
\frac{Γ^{+} ⊢_{n+1} t : A}{Γ ⊢_{n} Λ_{Γ,A}(t) : ∀(A)} (Λ)  \frac{Γ ⊢_{n} t : ∀(A)  n ⊢ B}{Γ ⊢_{n} App_{Γ,A}(t, B) : A[B]} (App)

The type annotations simplify the interpretation of the syntax. We may drop the annotations when they are clear from the context and write ts for app_{Γ,A,B}(t, s) and tB for App_{Γ,A}(t, B).

For any n we define a category of terms 𝕋_{n}^{0} whose objects are contexts n ⊢ Γ and morphisms between Γ and Δ are context morphisms, i.e. sequences of terms Γ ⊢ t_{i} : Δ_{i}. Composition of context morphisms is defined as usual as simultaneous substitution which can be defined by structural induction over the syntax. The categories 𝕋_{n}^{0} have products given on objects by juxtaposition of contexts. As in the case of the category of type substitutions we introduce the special syntax t[s] for substitution of a single term into another term (t[s] = t ∘⟨id , s⟩) and s^{+X} for weakening with the type X, i.e. s^{+X} = s ∘ π_{Γ,X}. If Γ.A ⊢_{n} t : B and Γ ⊢ s : A then Γ ⊢_{n} t[s] : B and Γ.X ⊢ s^{+X} : A. We also extend type substitution and weakening to terms in the obvious way, i.e. if Γ ⊢_{n+1} t : A and n ⊢ B then Γ[B] ⊢_{n} t[B] : A[B] and if Γ ⊢_{n} t : A then Γ^{+} ⊢_{n+1} t^{+} : B^{+}. More generally, if A⃗ ∈ 𝕊(m, n) and Γ ⊢_{n} t : A then we have Γ[A⃗] ⊢_{m} t[A⃗] : A[A⃗]. In this way we obtain an indexed category 𝕋^{0} : 𝕊^{op} → Cat (with fibres 𝕋_{n}^{0}). We also write 𝕋^{0} for the total category of the associated split fibration, i.e. the category 𝕋^{0} has as objects pairs [n, Γ] where n ⊢ Γ and a morphism from [n, Γ] to [m, Δ] is a pair [A⃗, t⃗] such that A⃗ ∈ 𝕊(n, m) and t⃗ ∈ 𝕋_{n}^{0}(Γ, Δ[A⃗]).

2.1 Equational theory

For t, s such that Γ ⊢_{n} t, s : A we define a conversion relation conv_{Γ,A} by the least congruence containing the following equations :

app_{Γ,A,B}(λ_{Γ,A,B}(t), s) conv_{Γ,B} t[s]
λ_{Γ,A,B}(app_{Γ,A,B}(t^{+A}, 0_{Γ.A})) conv_{Γ,A→B} t
App_{Γ,A}(Λ_{Γ,A}(t), B) conv_{Γ,A[B]} t[B]
Λ_{Γ,A}(App_{Γ,A}(t^{+}, 0)) conv_{Γ,∀(A)} t

For n ∈ ℕ we define the category 𝕋_{n} as the quotient of 𝕋_{n}^{0} by conv. The objects of 𝕋_{n} are contexts n ⊢ Γ and the morphisms are conv-equivalence classes of 𝕋_{n}^{0}-morphisms, i.e. tuples of terms. Since conv is a congruence it is respected by weakening and substitution so that these operations lift to equivalence classes. We identify notationally classes with representatives. In this way, we obtain another indexed category 𝕋 : 𝕊^{op} → Cat together with the associated split fibration 𝕋 → 𝕊.

2.2 The category of variable renamings

For n ⊢ Γ and n ⊢ Δ we define 𝕍_{n}(Γ, Δ) as the set of those morphisms in 𝕋_{n}(Γ, Δ) which consist of variables (natural numbers) only, i.e. do not contain the term formers app, λ, etc. Clearly, these morphisms are closed under composition and contain the identities so that we have an indexed sub-category 𝕍 of 𝕋 and 𝕋^{0}. The composition of the inclusion from 𝕍 into 𝕋^{0} with the projection from 𝕋^{0} to 𝕋 furnishes a product-preserving functor I from 𝕍 to 𝕋. We do not assume that I is monic although this follows a posteriori from our normalisation argument. Again, 𝕍 also denotes the total category of the associated split fibration. Objects of 𝕍 are pairs [n, Γ] where n ⊢ Γ and morphisms between [n, Γ] and [m, Δ] are pairs [A⃗, w] with A⃗ ∈ 𝕊(n, m) and w ∈ 𝕍_{n}(Γ, Δ[A⃗]).

Notice that the total categories 𝕍, 𝕋^{0}, and 𝕋 each have products by “abstract nonsense” since the total category of a fibration has finite products if the base and each fibre has finite products and reindexing preserves them. For example, the product of [n, Γ] and [1, ⋄] is given by [n + 1, Γ^{+}] with projections [π_{n,1}, id_{Γ}] and [π′_{n,1}, ⟨⟩].

Our glued model will be internal to the presheaf category 𝕍̂. The argument to be made would also go through with the more economic sub-category of weakenings (used in (Altenkirch, Hofmann, and Streicher 1995)) which consists of order-preserving variable renamings, i.e. the vectors of the form (i_{m−1}, … i_{0}) where i_{m−1} ≥ i_{m−2} ≥ ⋯ ≥ i_{0}. Using this category would, however, make the exposition more complicated, in particular in Section 8.2, so that we have opted for 𝕍. If an efficient algorithm is to be extracted from our development then the category of weakenings (or even the category of projections to initial segments, which also works albeit with a yet more complex development) should be used instead.

2.3 Normal forms and neutral terms

The sets NF and NE of normal forms and neutral terms, respectively, are given by the following grammar (where t ∈ NF and u ∈ NE and i ∈ ℕ):

NF ::= u | λ_{Γ,A,B}(t) | Λ_{Γ,A}(t)
NE ::= i | app_{Γ,A,B}(u, t) | App_{Γ,A}(u, B)

Notice that normal forms and neutral terms are stable under type substitution and variable renamings in the sense that if [A⃗, w] ∈ 𝕍([n, Γ], [m, Δ]) and t ∈ NF satisfies Δ ⊢_{m} t : A then the term Γ ⊢_{n} t[A⃗][w] : A[A⃗] is in normal form, too. The same goes for neutral terms. There can be more than one normal form in each conversion class; for an example see Section 8.3. The reason is that a normal form of universally quantified type can either be neutral (for instance a variable) or a Λ-abstraction.

3 Constructive metalanguage

We understand the previous and the following definitions to be made within a constructive metalanguage which contains an impredicative universe Prop of small sets closed under inductive definitions. Impredicativity means that the product of an arbitrary family of small sets is again small. Furthermore, we require subset types for equality predicates (i.e. equalisers) and quotients of classical (i.e. ¬¬-closed) equivalence relations. A model for such a metalanguage is furnished by ω-sets and pers/modest sets as described in (Streicher 1991). For a proof that the ω-set model admits the required quotients see for instance Ch. II of loc. cit.

We use an informal (impredicative) extensional Martin-Löf type theory to denote constructions in the metalanguage. In particular, we write Π and Σ for dependent product and sum, and we use λ and juxtaposition for abstraction and application and ⟨−, −⟩ and .1, .2 for pairing and projections. We use the symbol Type for the universe of sets in the metalanguage and we form kinds like A → Type to denote the class of families of sets indexed over A. If B : A → Type and f(x), g(x) : B(x) if x: A then we write {x: A | f(x) = g(x)} for the subset of A where f and g agree.

We use the symbols ∈ and : for membership interchangeably but mostly employ the colon when Martin-Löf type theory is being used.

Many of our constructions are taking place in specific models of our metalanguage. We overload the syntax of the type theoretic operations but may disambiguate by T ype^{C}, Π^{C}, Σ^{C} where C is the model. Since the models are defined inside our constructive metalanguage all internal constructions can be expanded and replaced by much longer (and unreadable) definitions in the metalanguage.

If a: A and f(a) = g(a) then we may write a : {x: A | f(x) = g(x)}. Conversely, if a : {x: A | f(x) = g(x)} then a : A and furthermore f(a) = g(a) may be inferred. If A is a small set then so is {x: A | f(x) = g(x)}.

For the definition of functions we either use λ-notation like in f = λx: A.t or equivalently a “pointwise” notation like in f(x: A) = t. For iterated application we sometimes use parentheses and commas, e.g. if f : A → Πb: B.C(b) and a: A and b: B then we may write f(a, b) instead of f a b. We sometimes omit arguments which can be inferred. For instance, if f : Πa: A.B(a) → C and a: A and b: B(a) then we may abbreviate f(a, b) by f(b).

4 Naive F -doctrines

Definition 1 A contextual cartesian closed category (ConCCC) is a category C together with a distinguished sub-class Ty = Ty^{C} such that

• C has a terminal object,

• C has all cartesian products of the form Γ × A where Γ ∈ C and A ∈ Ty,

• C has all exponentials of the form A ⇒ B for A, B ∈ Ty

Every cartesian-closed category C is a ConCCC with the setting Ty = |C|. The advantage of ConCCC’s over cartesian-closed categories is that term models furnish more naturally a ConCCC.

Proposition 2 The indexed category 𝕋 : 𝕊^{op} → Cat from Section 2 is an indexed ConCCC, i.e. 𝕋 : 𝕊^{op} → ConCCC where ConCCC is the category of ConCCC’s and structure-preserving functors. Moreover, the functors 𝕋(π_{n+1,n}) : 𝕋_{n} → 𝕋_{n+1} have right adjoints satisfying the Beck-Chevalley condition up to equality, i.e. 𝕋 admits split Cons_{1}-products in the sense of Jacobs (1991, §1.5). Moreover, 0 ∈ 𝕋_{1} is a generic object for 𝕋.

Proof. Standard. See, e.g. (Crole 1993). For the ease of the reader we give some of the raw data here. The cartesian product of Γ and A in 𝕋_{n} is given by the context Γ.A. The exponential of B by A in 𝕋_{n} is given by the type A ⇒ B. Finally, the result of applying the right adjoint of 𝕋(π_{n+1,n}) to A ∈ 𝕋_{n+1} is the type ∀(A) ∈ 𝕋_{n}. If t ∈ 𝕋_{n+1}(Γ^{+}, A) then its transpose is the term Λ_{Γ,A}(t) ∈ 𝕋_{n}(Γ, ∀(A)).

Notice that we have |𝕋_{n}| = 𝕊(n, 1) which establishes that 0 ∈ 𝕋_{1} (recall that 0 refers to the single type variable corresponding to the judgement ⊢_{1} 0) is a generic object. □

For further reference we call such a structure an external model. We remark that up to the distinction between contexts and types 𝕋 is a model of system F in the sense of Seely (Crole 1993). For the subsequent development it is, however, more appropriate to employ a different, but equivalent notion of model due to Asperti and Longo (1992) based on internal categories. Their notion is adapted to the ConCCC-situation in the following definition where the model of our metalanguage plays the role of their ambient category.

Definition 3 A naive F -doctrine is a ConCCC C which has Ty-indexed products of types, i.e. for every function B : Ty → Ty the product of B in C exists and lies in Ty.

Let C be a naive F -doctrine. In the following we introduce some notation and names to refer to its components. The objects of C are called contexts, the objects in Ty are called types. We write ⋄ for the terminal object and ⟨⟩_{Γ} ∈ C(Γ, ⋄) for the unique morphism into ⋄. If Γ is a context and A is a type then we write Γ.A for their cartesian product and π_{Γ,A} ∈ C(Γ.A, Γ) and π′_{Γ,A} ∈ C(Γ.A, A). If Δ = ⋄.A_{1}. . . . .A_{k} for types A_{i} then the cartesian product of Γ and Δ also exists in C and we write it as Γ.Δ and use the already introduced notation for the associated morphisms with the A-subscript replaced by Δ. We (partially) omit these and subsequent subscripts wherever appropriate.

If A and B are types then we write A ⇒ B for their exponential in C. If f ∈ C(Γ, A ⇒ B) and g ∈ C(Γ, A) then we write app_{Γ,A,B}(f, g) ∈ C(Γ, B) for the composition of ⟨f, g⟩ with the evaluation morphism. If f ∈ C(Γ.A, B) then we write λ_{Γ,A,B}(f) ∈ C(Γ, A ⇒ B) for the exponential transpose of f.

For B : Ty → Ty we write ∀(B): Ty for the product of B and for every X: Ty we write App_{B}(X): C(∀(B), B(X)) for the product projection corresponding to X. If f : ΠX: Ty.C(Γ, B(X)) is a Ty-indexed family of morphisms then Λ_{B}(f) : C(Γ, ∀(B)) denotes the (unique) morphism such that for all X: Ty

App_{B}(X) ∘ Λ_{B}(f) = f(X) Ty-Beta

Whenever f: C(Γ, ∀(B)) then we have

Λ_{B}(λX: Ty.App_{B}(X) ∘ f) = f Ty-Eta

We decorate these symbols with superscripts^{C} identifying the corresponding naive F -doctrine wherever this appears appropriate. Instead of C(A, B) we may write Mor(A, B) or Mor^{C}(A, B) for the set of morphisms.

Example 4 An example of a naive F -doctrine is furnished by the category P which has as objects the small sets (elements of Prop) and as morphisms the functions between them. We put Ty^{P} = |P| = Prop. It is clear that this defines a ConCCC. As for type quantification we use the impredicativity of Prop, i.e. for B : Prop → Prop we define ∀(B) as ΠX: Prop.B(X).

5 Interpretation of the syntax

Fix a naive F -doctrine C. By induction over the syntax we define a many-sorted interpretation function [[−]] = [[−]]^{C} which maps a context Γ in n free type variables to a function [[n ⊢ Γ]] from

[[n ⊢ ⋄]](X⃗: (Ty^{C})^{n})  = ⋄
[[n ⊢ Γ.A]](X⃗)  = [[n ⊢ Γ]](X⃗).[[n ⊢ A]](X⃗)
[[n ⊢ i]](X⃗) = X_{i} where X⃗ = (X_{n−1}, … X_{0})
[[n ⊢ A → B]](X⃗)  = [[n ⊢ A]](X⃗) ⇒ [[n ⊢ B]](X⃗)
[[n ⊢ ∀(A)]](X⃗)  = ∀(λX: Ty^{C}.[[n + 1 ⊢ A]](⟨X⃗, X⟩)
[[Γ ⊢_{n} i_{Γ} : Γ_{i}]](X⃗)  = projection from [[n ⊢ Γ]](X⃗) to [[n ⊢ Γ_{i}]]
[[Γ ⊢_{n} λ_{Γ,A,B}(t)]](X⃗)  = λ([[Γ.A ⊢_{n} t : B]](X⃗)
[[Γ ⊢_{n} app_{Γ,A,B}(t, s)]](X⃗)  = app([[Γ ⊢_{n} t : A]](X⃗), [[Γ ⊢_{n} s : B]](X⃗))
[[Γ ⊢_{n} Λ_{Γ,A}(t) : ∀(A)]](X⃗)  = Λ(λX: Ty^{C}.[[Γ^{+} ⊢_{n+1} t : A]](⟨X⃗, X⟩)
[[Γ ⊢_{n} App_{Γ,A}(t, B) : A[B]]](X⃗) = App([[Γ ⊢_{n} t : ∀(A)]](X⃗), [[n ⊢ B]](X⃗))

Figure 1: Interpretation of F_{βη}

(Ty^{C})^{n} to |C| and a type A in n free variables to a function [[n ⊢ A]] from (Ty^{C})^{n} to Ty^{C}. A term t in n free type variables and in context Γ of type A is mapped to a (dependent) function [[Γ ⊢_{n} t : A]] of type

ΠX⃗: (Ty^{C})^{n}.𝕋_{n}([[n ⊢ Γ]](X⃗), [[n ⊢ A]](X⃗))

The semantic equations are straightforward: syntactic constructs are interpreted by their semantic counterparts. The details are given in Fig. 5.

Theorem 5 (Soundness) The interpretation is sound, i.e. the interpretation functions are total in the domains described above and conversion is reflected by equality in the model: If t conv_{Γ,A} s then [[Γ ⊢_{n} t : A]] = [[Γ ⊢_{n} t : A]].

Proof. By induction on derivations. □

6 Presheaves as a model of the constructive metalanguage

The notions of ConCCC and naive F -doctrine make sense in any model of the constructive metalanguage. Of particular interest are categories of presheaves K̂ and categories of the form Fam(K̂) of families of presheaves over K. We explain how these categories model the constructive metalanguage and introduce some notation.

6.1 Categories of presheaves

Let K be a small category. It is well-known that the category K̂ = Set^{Kop} of presheaves supports extensional Martin-Löf type theory together with inductive definitions even if the ambient settheoretic universe with respect to which K̂ is formed is not a topos, but only a model of Martin-Löf type theory itself. We do not require quotient types on the level of presheaf categories. We refer to (Phoa 1992) for the precise definition of the interpretation of Martin-Löf type theory in a category of presheaves and only sketch some important aspects here. Dependent types in K̂ can be understood via the equivalence of categories (Moerdijk and Lane 1992, p. 157)

K̂/F ≅ { \atop El(F)}

where El(F) = y ↓ F is the category of elements of the presheaf F. It has as objects pairs (X, f) where f ∈ F_{X} and a morphism from (X, f) to (X′, f′) is a K-morphism u : X → X′ such that F_{u}(f′) = f. (We use subscripts for application of presheaves.) We write K̂(F) for { \atop El(F)}. So for example the objects of kind F → TypeK̂ are the objects of K̂(F). Cartesian products and Σ-types are taken pointwise: (U × V)_{I} = U_{I} × V_{I} and (Σu: U.V (u))_{I} = Σu: U(I).V_{I}(u). The same goes for subset types.

If U ∈ K̂(F) we write F_{I}(u) (instead of F_{(I,u)}) for the application of F to the pair (I, u). We sometimes call I a “stage” or a “world”.

The function space of U, V ∈ K̂ is given by the presheaf which sends I ∈ K to the set K̂(y(I) × U, V), where y : K → K̂ is the Yoneda embedding. More elementarily, the elements of (U → V)_{I} are mappings

μ ∈ ΠJ: K.K(J, I) × U_{J} → V_{J}

such that whenever u ∈ K(J, I), u′ ∈ K(J′, J), and f ∈ U_{J} then V_{u′}(μ_{J}(u, f)) = μ_{J′}(u ∘ u′, U_{u′}(f)).

We remark that by “uncurrying” a global element of a presheaf exponential, i.e. a natural transformation 1 ⟶ (U → V) is nothing but a natural transformation from U to V. More generally, since U → (V → W) is isomorphic to (U × V) → V a global element of U → (V → W) can be given by specifying a natural transformation from U × V to W. The same goes for longer chains of arrows.

This generalises to “non-empty contexts” in view of the definition of K̂(F) as a category of presheaves, i.e. the local exponential of G, H ∈ K̂(F) can be obtained by replacing K by El(K) in the definition of ordinary exponentials. We finally remark that dependent products can be obtained as regular subsets of suitable exponentials, e.g. if U ∈ K̂ and V ∈ K̂(U) then the dependent product Πu: U.V (u) ∈ K̂ equals {f : U → Σu: U.V (u) | −.1 ∘ f = id_{U}}.

This means that global elements of dependent products can also be given element-wise.

6.2 Impredicative universe

Less well-known is the existence of a small impredicative universe in K̂. Call a presheaf F ∈ K̂ “small” if for every I ∈ K the set F_{I} is small, i.e. lies in Prop. More generally, if G is any presheaf, we can consider the set Small(G) of small presheaves in K̂(G). An element of Small(G) is a functor from the opposite of the category El(G) of elements of G to the category of small sets. The operation Small(−) extends to a functor from (K̂)^{op} to the category of sets by putting for α : G′ → G and F ∈ Small(G)

Small(α)(F)_{I}(g) = F (I, α_{I}(g))

and if u : I′ → I and thus u ∈ El(G′)((I′, G′_{u}(g)) , (I, g)) and

Small(α)(F)_{u}(f) = F_{u}(f)

which works because u ∈ El(G)((I′, G_{u}(α_{X′}(u))) , (I, α_{I}(u))) by naturality of α. It is obvious that the product of a family of small presheaves is again small because its construction only involves taking products of small sets. The important point is that the small families are representable:

Theorem 6 The small presheaves over G are in bijective correspondence with K̂-morphisms from G to the presheaf Prop defined by Prop_{I} = Small(y(I))

Proof. If F ∈ Small(G) then the associated morphism χ_{F} : G → Prop at I ∈ K sends g ∈ G_{I} to the composition F ∘ ḡ where ḡ : K/I → El(G) maps u : J → I to (J, G_{u}(g)).

Conversely, if f : G → Prop then we obtain Prf (f) ∈ Small(G) as the presheaf which at (I, g) ∈ El(G) is f_{I}((I, g), id_{I}).

For F ∈ Small(G) we have Prf (χ_{F}) = F by functoriality of G and for f : G → Prop we have χ_{Prf (f)} = f by naturality of f. □

We shall henceforth identify small presheaves with the associated morphisms into Prop and use the informal Martin-Löf type theory explained above in Sect. 3 also to denote constructions in presheaf categories.

6.3 Interpretation of the syntax in a naive F -doctrine inside K̂

Assume a naive F -doctrine C inside some category of presheaves K̂. This means that we have a presheaf |C| ∈ K̂ (internally |C| : TypeK̂), a sub-presheaf Ty^{C} ⊂ |C|, and a presheaf C ∈ K̂(|C|, |C|) of morphisms (internally C : |C|×|C| → TypeK̂), as well as the constants specified after Def. 1 whose types are now understood w.r.t. the internal language of K̂. We remark that this amounts to an internal model in the sense of (Asperti and Martini 1992) with ambient category K̂. Following §5 of loc. cit. we define by induction on derivations a semantic function [[−]] = [[−]]^{C} which to n ⊢ Γ associates a K̂-morphism from (Ty^{C})^{n} to |C|, i.e. we have

[[n ⊢ Γ]] ∈ K̂((Ty^{C})^{n}, |C|) Viewed externally, [[n ⊢ Γ]] assigns to I ∈ K and X⃗ ∈ (Ty_{I}^{C})^{n} an element [[n ⊢ Γ]]_{I}(X⃗) ∈ |C|_{I} natural in I. The same goes for types. A term Γ ⊢_{n} t : A gets interpreted as a global element of the presheaf

ΠX⃗: (Ty^{C})^{n}.C([[n ⊢ Γ]](X⃗), [[n ⊢ A]](X⃗)) Externally, this is an assignment which to I ∈ K and X⃗ ∈ (Ty^{C}(I))^{n} associates an element

[[Γ ⊢_{n} t : A]]_{I}(X⃗) ∈ C_{I}([[n ⊢ Γ]]_{I}(X⃗), [[n ⊢ A]]_{I}(X⃗)) again natural in I.As a typical example, we define here the interpretation of the ∀-operator. Suppose we are given [[n + 1 ⊢ B]] ∈ K̂((Ty^{C})^{n+1}, Ty^{C}). The exponential transpose cur([[n + 1 ⊢ B]]) is a morphism in K̂ from (Ty^{C})^{n} to the exponential Ty^{C} → Ty^{C}. Composition with the semantic ∀-operator yields the desired meaning of [[n ⊢ ∀(B)]]:

[[n ⊢ ∀(B)]] = ∀ ∘ cur([[n + 1 ⊢ B]]) As explained above, we can also use λ-notation to define morphisms in K̂. This leads to the more familiar looking definition

[[n ⊢ ∀(B)]] = λX⃗: (Ty^{C})^{n}.∀(λX: Ty^{C}.[[n + 1 ⊢ B]](X⃗, X)) where the λ-abstraction is interpreted in K̂. In this way we can understand all the other equations from Fig. 5 by reading the right-hand sides as definitions in the internal language of global elements. Again, we have the following soundness property:

Proposition 7 The interpretation of the syntax in a naive F -doctrine internal to a category of presheaves is sound in the sense that whenever Γ ⊢_{n} t = s : A then [[Γ ⊢_{n} t : A]] = [[Γ ⊢_{n} s : A]].

We remark that such interpretation function can be defined for naive F -doctrines living inside an arbitrary model E of the metalanguage provided that the set of E-functions from X to Y in E is a (constructive) set. We stress that this interpretation function is not directly an instance of the interpretation function defined in 5 above because unlike there syntax and semantics live in different ambient set-theoretic universes.

6.4 Families of presheaves

For a model E of the constructive metalanguage, for instance E = K̂, let Fam(E) denote the category whose objects are pairs A = (A^{syn}, A^{sem}) where A^{syn} : Type^{E} and A^{sem} ∈ A^{syn} → Type^{E}. A morphism from A to B is a pair f = (f^{syn}, f^{sem}) such that f^{syn}: A^{syn} → B^{syn} and f^{sem} : Πa: A^{syn}.A^{sem}(a) → B^{sem}(f^{syn}(a)). Composition and identities are taken component-wise. We call the first component of an object, respectively a morphism, the syntactic component, and use the term semantic component for the second one. This terminology is motivated from the fact that in subsequent applications the first components very often are syntactic objects whereas the second components are predicates on syntactic components or proofs of such properties. We have a functor Fst : Fam(E) → E which singles out the syntactic components, i.e. we have Fst(X) = X^{syn} for X an object or a morphism.

Such categories of families can be subsumed under categories of presheaves because of the equivalence

Fam(E) ≃ E^{2op}

where 2 is the category (in E) with two objects and one non-identity arrow. In the case where E itself is of the form K̂ we can avoid to consider presheaf-valued presheaves by employing the equivalence

Fam(K̂) ≃ { \atop K × 2}

From this we know immediately that families of presheaves furnish a model of the constructive metalanguage. For subsequent use we give the constructions of exponentials, dependent types, and dependent products in Fam(E) in terms of the internal language of E. If A, B are objects in Fam(E) then the exponential is defined by (A → B)^{syn} = A^{syn} → B^{syn} and (A → B)^{sem}(f: (A → B)^{syn}) = Πa: A^{syn}.A^{sem}(a) → B^{sem}(f^{syn}(a)). A type depending on A can be presented as a pair F = (F^{syn}, F^{sem}) where F^{syn} : A → Type^{E} and F^{sem} : Πa: A^{syn}.A^{sem}(a) × F^{syn}(a) → Type^{E}. The dependent product over such a family has syntactic component

Π(A, F)^{syn} = Πa: A^{syn}.F^{syn}(a)

and semantic component

Π(A, F)^{sem}(f: Π(A, F)^{syn}) = Πa: A^{syn}.Πa: A^{sem}(a).F^{sem}(a, a, f(a))

It is well-known and obvious from these settings that the functor Fst : Fam(E) → E preserves all the structure of a model of the constructive metalanguage.

We remark that Fam(E) can be seen as a category of proof-relevant logical predicates or ”‘deliverables”’ in the sense of (Burstall and McKinna 1993).

6.5 Interpretation of the syntax in a naive F -doctrine internal to Fam(E)

From Section 6.3 it is clear how to interpret the syntax in a naive F -doctrine internal to Fam(E). For subsequent use it is, however, appropriate to spell out the particular nature of this interpretation and to introduce some notation. Let C be a naive F -doctrine in Fam(E) (for E a model of the metalanguage). As Fst : Fam(E) → E preserves all the structure of a model of the metalanguage, in particular substitution and Π-types, the component-wise application of Fst to C furnishes a model Fst(C) internal to E. More precisely, we have |Fst(C)| = Fst(|C|) and so forth. From the definition of Fst and [[−]] it is immediate that the syntactic component of the interpretation in C coincides with the interpretation in Fst(C). We abbreviate ([[−]]^{C})^{sem} by [[−]]^{C}.

Let (X⃗, X⃗) : (Ty^{C})^{n}, i.e. X⃗ : (Ty^{FstC})^{n} and X⃗ : ((Ty^{C})^{sem})^{n}(X⃗). For n ⊢ Γ we have:

[[n ⊢ Γ]]^{C}(X⃗, X⃗) : |C|^{sem}([[n ⊢ Γ]]^{Fst(C)}(X⃗))

Similarly for types. A term Γ ⊢_{n} t : A gets interpreted as

[[Γ ⊢_{n} t : A]]^{C}(X⃗, X⃗) = C^{sem}([[Γ ⊢ t : A]]^{Fst(C)})

7 Sconing of a naive F -doctrine

Fix a naive F -doctrine C living in some model of type theory E. Our aim is to define a new doctrine Sc = Sc(C) internal to Fam = Fam(E) in such a way that the model C arises as Fst(Sc(C)).

Therefore, there is no need to define the syntactic components as they are fixed by this specification. Accordingly, we omit the ^{sem} superscript in the definition of the semantic components.

For Γ: |C| we write Sect(Γ) for C(1, Γ)—the set of global elements of Γ. We define

|Sc|(Γ: |C|) = Sect(Γ) → Prop

This means that the object of objects takes the form (|C|, λΓ: |C|.Sect(Γ) → Prop). The semantic component of the family of morphisms in Sc is defined by

Sc(Γ: |C|, Γ: Sc(Γ), Δ: |C|, Δ: Sc(Δ), f: C(Γ, Δ)) =

Πγ: Sect(Γ).Γ(γ) → Δ(f ∘ γ)

The object of types Ty^{Sc} is the restriction of |Sc| to types, i.e. we have Sc^{Ty}(A: Ty^{C}) = Sect(A) → Prop.

We come to composition. If Γ: Sc(Γ), Δ: Sc(Δ), Θ: Sc(Θ), and f: C(Γ, Δ) and g: C(Δ, Θ) and furthermore f: Sc(Γ, Δ, f) and g: Sc(Δ, Θ, g) then we define the semantic component of the composition of f and g by

λγ: Sect(Γ).λγ: Γ(γ).g(f ∘ γ, f(γ, γ)) : Θ((g ∘ f) ∘ γ)

Associativity of composition in C is required for this to “type-check”. Similarly, we define identity morphisms and the axioms for a category are readily verified.

Notice that this construction amounts to the well-known sconing construction (glueing along the global sections functor) as discussed extensively in (Lambek and Scott 1985; Crole 1993). There the glued category lives inside Set, but as there is a structure-preserving functor from the glued category back to the original one this amounts to specifying a category internal to Fam(Set). The construction of the products and exponentials in our Sc is as in the abovementioned sources. We give their definitions on objects but omit the associated morphisms and the verifications.

For Γ ∈ Sc(Γ) and A ∈ Ty^{Sc}(A) and B ∈ Ty^{Sc}(B) we define

(Γ.A)(⟨γ, x⟩ ∈ Sect(Γ.A)) = Γ(γ) × A(x)

(A ⇒ B)(f: Sect(A ⇒ B)) = Πx: Sect(A).A(x) → B(app(f, x))

Now we will show that Sc has the required Ty-indexed products as a category internal to Fam. Let B : Ty^{C} → Ty^{C} together with B : ΠX: Ty^{C}.Ty^{Sc}(X) → Ty^{Sc}(B(X)) be an endomorphism of the object of types in Sc. We claim that the semantic component of the product is given by

∀(B, B, t: Sect(∀(B))) = ΠX: Ty^{C}.ΠX: Ty^{Sc}.B(X, X, App(X) ∘ t)

It remains to define type abstraction and application and to check the equations. For X: Ty^{C} and X: Ty^{Sc}(X) the semantic component of the application morphism is defined by

App(X, X) = λt: Sect(∀(B)).λt: ∀(B, B, t).t(X, X) : X(App(X) ∘ t) Conversely, if Γ: Sc(Γ) and f: ΠX: Ty^{C}.C(Γ, B(X)) and

f : ΠX: Ty^{C}.ΠX: Ty^{Sc}(X).Sc(Γ, Γ, B(X), B(X, X), f(X)) is a family of morphisms in Sc then we define

Λ(f) = λγ: Sect(Γ).λγ: Γ(γ).λX: Ty^{C}.λX: Ty^{Sc}(X).f(γ, γ, X, X) :

Sc(Γ, Γ, ∀(B), ∀(B, B), Λ(f))

For this to “type-check” the identity App(X) ∘ Λ(f) ∘ γ = f(X) ∘ γ—a consequence of Ty-Beta has been used. The required equations are straightforward.

7.1 Interpretation of the syntax in Sc(C)

By construction of Sc(C) one has Fst(Sc(C)) = C. Thus, due to the analysis in Section 6.4, the interpretation in Sc(C) gives rise to a (many-sorted) function [[−]]^{Sc} which maps

• A judgement n ⊢ Γ to a function

[[n ⊢ Γ]]^{Sc} : ΠX⃗: Ty^{n}.ΠX⃗: (Ty^{Sc})^{n}(X⃗).Sect([[n ⊢ Γ]]^{C}(X⃗)) → Prop

• A judgement Γ ⊢_{n} t : A to a function [[n ⊢ t : A]]^{Sc} : ΠX⃗: Ty^{n}.ΠX⃗: (Ty^{Sc})^{n}(X⃗).

Πγ: Sect([[n ⊢ Γ]]^{C}(X⃗)).Πγ: [[n ⊢ Γ]]^{Sc}(X⃗, X⃗, γ).[[n ⊢ A]]^{Sc}(X⃗, X⃗, [[Γ ⊢_{n} t : A]]^{C} ∘ γ)

Again, the equational theory is respected in the sense that convertible terms are mapped to the same semantic objects.

8 Exploring 𝕍̂

We will now explore the specific features of the presheaf category 𝕍̂. Our aim is to isolate a context of definitions and equations which enables to carry out the construction of the model GT entirely within the internal language of 𝕍̂, i.e. using the constructive metalanguage augmented by this context of definitions. We start by lifting the term model 𝕋 to a naive F -doctrine T inside 𝕍̂ equipped with a higher-order abstraction operator. Secondly, we define sets and constructors of normal forms and neutral terms together with the associated embeddings.

8.1 The term model

Before giving the explicit definition of T we describe its construction in more abstract terms. This enables us to use existing results for the verification that T actually is a naive F -doctrine internal to 𝕍̂. Afterwards, we give the explicit definitions of (most of the) structure components of T for further reference and ease of the reader.

The abstract categorical construction of T proceeds in two steps. We start from the split fibred ConCCC 𝕋 : 𝕊^{op} → Cat with Cons_{1}-products. Following (Asperti and Martini 1992) we call such a structure an external model for further reference. To this fibration we apply the constant family construction from (Jacobs 1991, §4.4.4) together with restriction along 𝕍 resulting in an external model 𝕋//𝕍 now over 𝕍 and with type object [1, ⋄] ∈ 𝕍. The objects of (𝕋//𝕍)_{[n,Γ]} are the objects of 𝕋_{n}; a (𝕋//𝕍)_{[n,Γ]}-morphism from Δ to Θ is a 𝕋_{n}-morphism from Γ.Δ to Θ.

The definition of composition and identities in 𝕋//𝕍 uses the cartesian products in 𝕋. For example, the identity morphism at Δ ∈ (𝕋//𝕍)_{[n,Γ]} is the product projection (in 𝕋_{n}) from Γ.Δ to Δ. The composition of f ∈ 𝕋//𝕍_{[n,Γ]}(Δ, Θ) (hence f ∈ 𝕋_{n}(Γ.Δ, Θ)) with g ∈ 𝕋//𝕍_{[n,Γ]}(Θ, Υ) is given by the morphism g ∘⟨π_{Γ,Δ}, f⟩ in 𝕋_{n}.

Products and exponentials are inherited from 𝕋.

From the development in loc. cit. adapted to the case of ConCCC’s together with the fact that I : 𝕍 → 𝕋 preserves finite products it follows that this is a split fibred ConCCC.

We now show directly that 𝕋//𝕍 is an external model. The generic object is given by 0 ∈ 𝕍_{[1,⋄]}. Recall from Section 2 that the product in 𝕍 of [n, Γ] and [1, ⋄] is [n + 1, Γ^{+}]. If B ∈ 𝕋//𝕍_{[n+1,Γ^{+}]} then we have ∀(B) ∈ 𝕋//𝕍_{[n,Γ]}. Furthermore, if Δ ∈ 𝕋//𝕍_{[n,Γ]} and f : 𝕋//𝕍_{[n+1,Γ^{+}]}(Δ^{+}, B), i.e. f : 𝕋//𝕍_{n+1}(Γ^{+}.Δ^{+}, B), then Λ_{Γ.Δ,B}(f) : 𝕋//𝕍_{[n,Γ]}(Δ, ∀(B)) is the transpose of f for the desired adjunction. The counit of the adjunction is given by application, i.e. App(0_{Γ^{+}.∀(B)^{+}}, 0) : 𝕋//𝕍_{[n+1,Γ^{+}]}(∀(B)^{+}, B).

The desired model T is now obtained by applying the process of internalisation from (Asperti and Martini 1992) to the external model 𝕋//V resulting in a naive F -doctrine internal to 𝕍̂. For further reference and for the reader not familiar with loc. cit. we explicitate parts of the raw data of T .

Its object of contexts is the presheaf Con defined by Con_{[n,Γ]} = {Δ | n ⊢ Δ}(= |𝕋_{n}|) Con_{[A⃗,w]}(Δ) = Δ[A⃗] if [A⃗, w] ∈ 𝕍([m, B], [n, Γ]) and ⊢_{n} Δ The sub-presheaf of types Ty ⊂ Con is defined by

Ty_{[n,Γ]} = {A | ⊢_{n} A}(= Ty^{𝕋_{n}})

Its family of morphisms Mor : Con × Con → Type is given by

Mor_{[n,Γ]}(Δ, Θ) = 𝕋_{n}(Γ.Δ, Θ)

as convertibility classes of syntactic context morphisms. If [A⃗, w] ∈ 𝕍([m, B], [n, Γ]) and t⃗ ∈ Mor_{[n,Γ]}(Δ, Θ) then we define

Mor_{[A⃗,w]}(t⃗) = t⃗[A⃗] ∘(w.Δ[A⃗])

From (Asperti and Martini 1992) the following result is now immediate.

Theorem 8 The category T is a naive F -doctrine internal to 𝕍̂.

Remark 9 The presheaf Sect(Δ) = Mor(⋄, Δ) has the following remarkable property. For ([n, Γ], Δ) ∈ 𝕍̂(Con) we have

Sect_{[n,Γ]}(Δ) = 𝕋_{n}(Γ, Δ)

so that the global sections in T correspond to vectors of open terms.

In order to explicitate the higher-order operations corresponding to type quantification and abstraction we require the following analysis of exponentiation with representable presheaves also used in (Asperti and Martini 1992).

Lemma 10 Let K be a category, A be an object of K, such that the products I × A exist for all I ∈ K and F ∈ K̂ be a presheaf. The exponential y(A) → F of F by the representable presheaf y(A) = K(−, A) is isomorphic to the functor F_{−×A}.

Proof. Immediate from the definition of exponentials in presheaf categories and the fact that the Yoneda embedding preserves products. □

Lemma 11 Let F be a presheaf in 𝕍̂. The exponential Ty → F in 𝕍̂ is isomorphic to the presheaf F^{Ty} given by F_{[n,Γ]}^{Ty} = F_{[n+1,Γ^{+}]}.

Proof. The presheaf Ty is isomorphic to the representable presheaf y([1, ⋄]). We conclude with Lemma 10 □

To keep the exposition simple we shall henceforth treat the isomorphisms guaranteed by the above results as identities.

We now construct the required function ∀ : (Ty → Ty) → Ty in a pointwise way. Assume [n, Γ] ∈ 𝕍 and B : (Ty → Ty)_{[n,Γ]}. From Lemma 11 we know that in fact B : Ty_{[n+1,Γ^{+}]}, i.e. n + 1 ⊢ B. We put

∀_{[n,Γ]}(B) = ∀(B) : {X | n ⊢ X} = Ty_{[n,Γ]}

Naturality is immediate from the compatibility of type quantification with substitution and weakening.

In a similar way we define type abstraction and application following the settings in the external version 𝕋//𝕍.

Proposition 12 (Interpretation in T ) Suppose that [m, Δ] ∈ 𝕍 and X⃗ ∈ 𝕊(m, n)(= Ty_{[m,Δ]}^{n}) . If n ⊢ Γ then

[[n ⊢ Γ]]_{[m,Δ]}(X⃗) = Γ[X⃗]

Furthermore, if Γ ⊢_{n} t : A then

[[Γ ⊢_{n} t : A]]_{[m,Δ]}^{T}(X⃗) = [t[X⃗] ∘ π_{Γ[X⃗],Δ}]_{conv} ∈ 𝕋_{m}(Γ[X⃗].Δ , A[X⃗])

In particular, if ⋄ ⊢_{0} t : A is a closed term then

[[⋄ ⊢_{0} t : A]]_{[0,⋄]}^{T}(⋆) = [t]_{conv}

Proof. Induction on derivations. □

8.2 The presheaf of variables

The term model as a naive F -doctrine can more simply be defined internal to 𝕊̂ by applying internalisation directly to the external model 𝕋. But that would not allow to have open terms of type A,i.e. generalised elements of A in 𝕋, being represented by Sect(A). It is this property that opens up the possibility to use the simple-minded sconing construction from Section 7 to prove existence of normal forms and not only of weak head normal forms as was done in (Coquand and Dybjer 1996). However, in order to make use of this fact without having to look at 𝕍̂ externally, we have to express this property in terms of the internal language. This will be done by reformulating λ-abstraction in T as a higher-order operation in 𝕍̂.

Had we worked internal to 𝕋̂ then we would have a canonical isomorphism between Sect(A) → Sect(B) and Sect(A ⇒ B) by an analogue of Lemma 11 since Sect(A) is representable, i.e. T would be a full internal subcategory of 𝕋̂. Unfortunately, Sect(A) is not representable in 𝕍̂. Yet, there exists a representable sub-presheaf Par(A) of Sect(A) corresponding to those open terms which are variables. This presheaf has the property that there is an isomorphism ℓ : (Par(A) → Sect(B)) → Sect(A ⇒ B) which is not as comfortable as a full internal subcategory but will suffice for our purposes. The reason for accepting this inconvenience is that normal forms are not closed under arbitrary substitutions and thus do not give rise to presheaves in 𝕋̂ but only in 𝕍̂.

Definition 13 The presheaf Par : 𝕍̂(Ty) is defined on objects by

Par_{[n,Γ]}(A) = 𝕍_{n}(Γ, A)

and for [A⃗, w] ∈ 𝕍([n′, Γ′] , [n, Γ]) and n ⊢ A and w′ ∈ 𝕍_{n}(Γ, A) we define

Par_{[A⃗,w]}(w′) = w′[A⃗] ∘ w ∈ Par_{[n′,Γ′]}(A[A⃗])

The natural transformation par : Par → Sect in 𝕍̂(Ty) is defined as the inclusion from weakenings into terms.

Lemma 14 The presheaf Par is represented by the object ([1, 0], 0) of El(Ty). For any object ([n, Γ], A) of El(Ty) the object ([n, Γ.A], A) is the cartesian product of ([n, Γ], A) and ([1, 0], 0).

Proof. Suppose ([n, Γ], A) is an object of El(Ty), i.e. n ⊢ Γ and n ⊢ A. By definition, an element of Par_{[n,Γ]}(A) is a renaming w ∈ 𝕍_{n}(Γ, A). It gives rise to the morphism [A, w] ∈ 𝕍([n, Γ] , [1, 0]) because 0[A] = A. Furthermore, by using 0[A] = A again, we have that [A, w] is in fact an El(Ty)-morphism from ([n, Γ], A) to ([1, 0], 0). For the converse, assume that [B, w] is an arbitrary El(Ty)-morphism from ([n, Γ], A]) to ([1, 0], 0), i.e. [B, w] ∈ 𝕍([n, Γ] , [1, 0]) and 0[B] = A then we must have B = A, thus w ∈ 𝕍_{n}(Γ, A) = Par_{[n,Γ]}(A). It is obvious that this establishes a natural isomorphism between Par and y(([1, 0], 0)).

For the second part we notice that Ty is representable by [1, ⋄] and therefore the category El(Ty) is isomorphic to the slice category 𝕍/[1, ⋄]. So the cartesian product in question amounts to the pullback of [A, ⟨⟩] : [n, Γ] → [1, ⋄] and [id_{1}, ⟨⟩] : [1, 0] → [1, ⋄]. This pullback can be obtained using a general construction, but we prefer to give it directly as follows:

[n, Γ.A] \overline{\begin{matrix}[A, π′_{Γ,A}] \\  \end{matrix}}[1, 0]

[figure: [n, Γ]; [id_{n}, π_{Γ,A}]; [A, ⟨⟩]; [1, ⋄]; [id_{1}, ⟨⟩]]

To see that the upper arrow is indeed a 𝕍-morphism notice again that 0[A] = A. It is clear that the square commutes. If [A⃗, w] : [m, Δ] → [n, Γ] and [B, w′] : [m, Δ] → [1, 0] is a cone then we must have w ∈ 𝕍_{m}(Δ, Γ[A⃗]) and w′ ∈ 𝕍_{m}(Δ, B) and (from the commutativity) B = A[A⃗]. The uniqe mediating morphism is then given by [A⃗, ⟨w, w′⟩] : [m, Δ] → [n, Γ.A]. □

Corollary 15 For every presheaf F ∈ 𝕍̂(Ty) the exponential Par → F is isomorphic to the presheaf which sends ([n, Γ], A) to F_{[n,Γ.A]}(A).

Proof. Immediate from Lemma 14 and Lemma 10. □

Proposition 16 There exists a natural transformation ℓ : ΠA, B: Ty.(Par(A) → Sect(B)) → Sect(A ⇒ B) such that the following equation holds in 𝕍̂

∀A, B: Ty.∀t: Sect(A ⇒ B) . t = ℓ(λp: Par(A).app(t, par(p)))

Proof. By Cor. 15 the arguments to ℓ at stage [n, Γ] amount to types n ⊢ A, B and a term t with Γ.A ⊢_{n} t : B. We define ℓ_{[n,Γ]}(A, B, t) as λ_{Γ,A,B}(t) and the required equation follows from Eta. □

As announced before ℓ is actually an isomorphism, i.e. for f : Par(A) → Sect(B) we have f = λp: Par(A).app(ℓ(f), p). However, we do not require this property for our purposes.

Remark 17 The presheaf Par together with ℓ can serve as an interpretation of the higher-order syntax for λ-calculus as described in (Despeyroux, Felty, and Hirschowitz 1995). As stated before, in a term model internal to 𝕋̂ the presheaf Sect(A) → Sect(B) is isomorphic to Sect(A ⇒ B) and one thus obtains a model for the usual higher-order abstract syntax of typed λ-calculus as described e.g. in (Harper, Honsell, and Plotkin 1993).

8.3 The presheaves of normal and neutral terms

As neutral terms and normal forms are stable under type substitutions and weakenings these sets induce presheaves over Con (and also over Ty) defined by

NF_{[n,Γ]}(Δ) = Tuples of normal forms of type Δ in context Γ NE_{[n,Γ]}(Δ) = Tuples of neutral terms of type Δ in context Γ

The clauses of the inductive definition of these sets induce natural transformations as given in the second part of Figure 8.3. These operations allow to build up normal forms and neutral terms in the internal language. Again, we have higher-order constructors giving normal forms of functional and polymorphic types. Notice that we do not have an induction principle for NE and NF in 𝕍̂. We also have functions i : ΠA: Ty.NF (A) → Sect(A) and k : ΠA: Ty.NE(A) → NF (A) and therefore also j : ΠA: Ty.NE(A) → Sect(A) defined as the composition i ∘ k. The functions j and i commute with the constructors in the obvious way. For instance, if p : Par(A) then

j(par_{NE}(p)) = par(p)

and if B: Ty → Ty and f: ΠX: Ty.NF (B(X)) then

i(Λ_{NF} (f)) = Λ(λX: Ty.i(f(X)))

In the case of λ_{NF} the higher-order abstractor ℓ is used: If A, B: Ty and f: Par(A) → NF (B) then

i(λ_{NF} (A, B, f)) = ℓ(j(ap_{NE}(u, v)))

Analogous equations hold for the remaining constructors of NE and NF .

We stress that the coercion i is not monic. For example

M_{1} := Λ_{NF} (λX: Ty.λ_{NF} (λp: Par(X ⇒ X).k(par_{NE}(p))))

and

M_{2} := Λ_{NF} (λX: Ty.λ_{NF} (λp: Par(X ⇒ X).λ_{NF} (λx: Par(X).k(ap_{NE}(par_{NE}(p), k(par_{NE}(x)))))

Externally, we have M_{1} = ΛX.λp.p and M_{2} = ΛX.λp.λx.app(p, x). These two are different normal forms of type ∀X.X ⇒ X but i(M_{1}) = i(M_{2}) by Eta.

We do not need that i is monic for the purposes of our proof; the fact that there can be different normal forms of the same conversion class simply means that our normalisation function will not be surjective, but simply picks out one particular normal form (in our example this will be M_{2}.) One could enforce uniqueness of normal forms by using an analogue of Huet’s long βη-normal forms (Huet 1976) which is, however, not unproblematic since these are not stable under type substitution. So the morphism part of the presheaf NF would have to perform certain η-expansions.

This completes the inspection of the internal language of 𝕍̂. The construction of the glued model to follow can now be carried out entirely on top of the definitions made so far and summarised in Figure 8.3.

9 The Tait model

Our aim is now to apply a mild variant of the sconing construction from Section 7 to the term model T . We do not consider arbitrary predicates over sections, but only those which are valid for all sections corresponding to neutral terms and which imply the existence of normal forms, i.e. a naive version of Tait’s computability predicates. More precisely, we define a naive F -doctrine GT internal to Fam(𝕍̂) the first component of which is the term model T , i.e. Fst(GT ) = T . The second component of the object of contexts Con^{GT} : Con → Type is defined as

λΓ: Con.ΣP: Sect(Γ) → Prop. (Πt: Sect(Γ).P (t) → {t′: NF (Γ) | i(t′) = t})×

(Πu: NE(Γ).P (j(u)))

If Γ: Con^{GT} (Γ) we refer to its three components by Γ^{pred}, q^{Γ}, and u^{Γ}, respectively. I.e. we have

Γ^{pred} : Sect(Γ) → Prop

and

q^{Γ} : Πt: Sect(Γ).Γ^{pred}(t) → NF (Γ)

in such a way that i(q^{Γ}(t, t)) = t. Finally, u^{Γ} : Πu: NE(Γ).Γ^{pred}(j(u)).

According to our convention on arguments which can be inferred we often omit the first argument to q.

Con : Type Ty : Type Mor : Con × Con → Type id : ΠΓ: Con.Mor(Γ, Γ) comp : ΠΓ, Δ, Θ: Con.Mor(Δ, Θ) × Mor(Γ, Δ) → Mor(Γ, Θ) ⋄ : Con ⟨⟩ : ΠΓ: Con.Mor(Γ, ⋄) −.− : Con × Ty → Con cons : ΠΓ: Con.ΠA: Ty.ΠΔ: Con.Mor(Δ, Γ) × Mor(Δ, A) → Mor(Δ, Γ.A) π : ΠΓ: Con.ΠA: Ty.Mor(Γ.A, Γ) π′ : ΠΓ: Con.ΠA: Ty.Mor(Γ.A, A) ⇒: Ty × Ty → Ty app : ΠA, B: Ty.ΠΔ: Con.Mor(Δ, A ⇒ B) × Mor(Δ, A) → Mor(Δ, B) λ : ΠA, B: Ty.ΠΔ: Con.Mor(Δ.A, B) → Mor(Δ, A ⇒ B) ∀ : (Ty → Ty) → Ty App : ΠB: Ty → Ty.ΠA: Ty.Mor(∀(B), B(A)) Λ : ΠB: Ty → Ty.ΠΔ: Con.(ΠX: Ty.Mor(Δ, B(X))) → Mor(Δ, ∀(B))

Equations stating that the above data define a naive F -doctrine

Par : Ty → Type par : ΠA: Ty.Par(A) → Sect(A) ℓ : ΠA, B: Ty.(Par(A) → Sect(B)) → Sect(A ⇒ B) ∀A, B: Ty.∀t: Sect(A ⇒ B). t = ℓ(λp: Par(A).app(t, par(p)))

NE, NF : Ty → Type par_{NE} : ΠA: Ty.Par(A) → NE(A) ap_{NE} : ΠA, B: Ty.NE(A ⇒ B) → NF (A) → NE(B) Ap_{NE} : ΠB: Ty → Ty.NE(∀(B)) → ΠX: Ty.NE(B(X)) proj_{NE} : ΠΓ: Con.ΠA: Ty.NE(Γ.A) → NE(Γ) var_{NE} : ΠΓ: Con.ΠA: Ty.NE(Γ.A) → NE(A) ⟨⟩_{NF} : NF (⋄) cons_{NF} : ΠΓ: Con.ΠA: Ty.NF (Γ) → NF (A) → NF (Γ.A) λ_{NF} : ΠA, B: Ty.(Par(A) → NF (B)) → NF (A ⇒ B) Λ_{NF} : ΠB: Ty → Ty.(ΠX: Ty.NF (B X)) → NF (∀(B)) i : ΠA: Ty.NF (A) → Sect(A) j : ΠA: Ty.NE(A) → Sect(A) k : ΠA: Ty.NE(A) → NF (A)

Equations specifying the interaction of i and j with the constructors of NE and NF

Figure 2: Internal language of 𝕍̂ We define Ty^{GT} : Ty → Type as the restriction of Con^{GT} to Ty. The second component of the object of morphisms is defined by

Mor^{GT} (Γ, Γ, Δ, Δ, f: Mor(Γ, Δ)) = Πγ: Sect(Γ).Γ^{pred}(γ) → Δ^{pred}(f ∘ γ)

Since the definition of Mor^{GT} does not depend on the added components q and u, the construction of products, exponentials, and type-indexed products can be carried out as in the case of Sc(T ) replacing Ty^{Sc} by Ty^{GT} in the case of the type-indexed products. It only remains to show that these constructions can be extended to “Tait-predicates”, i.e. the predicates are defined as before, but we need to give the q and u components. For the ease of the reader we reproduce the predicates themselves, as well.

First, we define

⋄^{pred}(x: Sect(⋄)) = {⋆}
q^{⋄}(x: ⋄^{pred}(x)) = ⟨⟩_{NF}
u^{⋄}(u: NE(⋄))  = ⋆

For Γ: Con, Γ: Con^{GT} (Γ), and A: Ty, and A: Ty^{GT} (A) we define

(Γ.A)^{pred}(⟨γ, x⟩: Sect(Γ.A)) = Γ^{pred}(γ) × A^{pred}(x)
q^{Γ.A}(⟨γ, x⟩: (Γ.A)(⟨γ, x⟩)) = cons_{NF} (q^{Γ}(γ), q^{A}(x))
u^{Γ.A}(u: NE(Γ.A))  = ⟨u^{Γ}(proj_{NE}(u)), u^{A}(var_{NE}(u))⟩

We come to exponentials. Let A, B: Ty, and A: Ty^{GT} (A) and B: Ty^{GT} (B). We define

(A ⇒ B)^{pred}(t: Sect(A ⇒ B)) = Πa: Sect(A).A^{pred}(a) → B^{pred}(app(t, a))
q^{A⇒B}(t: (A ⇒ B)^{pred}(t))  = λ_{NF} (λp: Par(A).q^{B}(t(p, u^{A}(par_{NE}(p)))))
u^{A⇒B}(u: NE(A ⇒ B))  = λa: Sect(A).λa: A^{pred}(a).u^{B}(ap_{NE}(u, q^{A}(a)))

To type-check the quote expression, we need to show that

i(λ_{NF} (λp: Par(A).q^{B}(t(p, u^{A}(par_{NE}(p)))))) = t

We calculate as follows. (The first argument to q will be given.)

i(λ_{NF} (λp: Par(A).q^{B}(app(t, par(p)) , t(p, u^{A}(par_{NE}(p))))))
= ℓ(λp: Par(A).i(q^{B}(app(t, par(p)) , t(p, u^{A}(par_{NE}(p))))))
= ℓ(λp: Par(A).app(t, par(p)))  by equation for ℓ
= t

Finally the type-indexed products. We require a generic Tait predicate for every type X; more precisely we define U : ΠX: Ty.Ty^{GT} (X) by

U(X)^{pred}(t: Sect(X)) = {t′: NF (X) | i(t′) = t}
q^{U(X)}(t: U(X)^{pred}(t)) = t
u^{U(X)}(u: NE(X))  = k(u)

Now for B: Ty → Ty and bB: ΠX: Ty.Ty^{GT} (X) → Ty^{GT} (B(X)) we define

∀(B)^{pred}(t: Sect(∀(B))) = ΠX: Ty.ΠX: Ty^{GT} (X).B(X, X)^{pred}(App(t, X))
q^{∀(B)}(t: ∀(B)^{pred}(t))  = Λ_{NF} (λX: Ty.q^{B(X,U(X))}(t(X, U(X))))
u^{∀(B)}(u: NE(∀(B)))  = λX: Ty.λX: Ty^{GT} (X).u^{B(X,X)}(Ap_{NE}(u, X))

10 The normalisation function

Theorem 18 For every closed type 0 ⊢ A there exists a constructively definable function nf_{A} mapping closed terms of type A to normal forms in such a way that if 0 ⊢ t : A then 0 ⊢ nf_{A}(t) = t : A and if 0 ⊢ t = t′ : A then nf_{A}(t) and nf_{A}(t′) are syntactically equal.

Proof. Consider the interpretation of the syntax in the model GT . We make the following definitions (in the constructive metalanguage, no longer in 𝕍̂). Recall that 𝕋_{0}(•, A) is the set {t | • ⊢_{0} t : A} modulo convertibility.

A^{pred}(t ∈ 𝕋_{0}(•, A)) = ([[0 ⊢ A]]^{GT})^{pred}_{[0,•]}(t, id_{[0,•]}) ∈ Prop
A^{quote}(t ∈ 𝕋_{0}(•, A)) = ([[0 ⊢ A]]^{GT})^{quote}_{[0,•]}(t) : A^{pred}(t) → {t′: NF (A) | i(t′) = t}

Now, if ⊢_{0} t : A then [[⊢_{0} t : A]]_{[0,•]}^{GT} : A^{pred}(t) and we define

nf_{A}(t) = A^{quote}([[⊢_{0} t : A]]_{[0,•]}^{GT})

These definitions are type-correct by Prop. 12.

From the type of A^{quote} we know that

i(nf_{A}(t)) = t

Furthermore, by the soundness of the interpretation in the Tait model the function nf maps convertible terms to equal normal forms. □

The restriction to closed types and terms is merely for ease of presentation. Open terms can be normalised by normalising their universal closures.

11 Conclusion

We have defined an internal model of system F the interpretation in which yields a normalisation function. The model uses the idea of glueing along the global sections functor (“Freyd sconing”), but had to be constructed internal to a category of presheaves where internal global sections correspond to open terms. In this way we were able to overcome the difficulties with full βη-reduction experienced in (Coquand and Dybjer 1996) where an ordinary set-theoretic semantic was used and thus reduction underneath an abstraction could not be catered for. Our method of using presheaves seems to be a general tool applicable in such situations. Furthermore, we have generalised the apporach in loc. cit. to polymorphism by considering presheaves not w.r.t. classical set theory, but relative to a model of impredicative type theory where polymorphic quantification has a natural interpretation as dependent product. We have employed the fact that the operation of passing to a presheaf model preserves the possibility of impredicative quantification cf. Prop. 6. Compared to (Altenkirch, Hofmann, and Streicher 1995) where presheaves were also used, we have in this paper used the internal language of the presheaf category for expressing the glueing construction. It appeared in the course of this work that due to the extra complication arising from type variables and polymorphism the argument is no longer manageable without using the internal language. The important point is that functional abstraction and type quantification are expressible as higher-order operations in this internal language. We have explained how this relates to higher-order abstract syntax for λ-calculus (Harper, Honsell, and Plotkin 1993; Despeyroux, Felty, and Hirschowitz 1995).

Our proof can be entirely formalised in extensional type theory, for instance Nuprl (Constable et al. 1986). One can also aim at a formalisation in intensional type theory like ALF or Lego, but then in order to define extensional objects like function spaces or the presheaf of convertibility classes one would have to use setoids, i.e. types with equivalence relations, as has been done in (Coquand 1994). Notice that such a formalisation would have to implement presheaves and natural transformations and not merely the internal language. All the definitions which for ease of exposition we have made in terms of the internal language have to be expanded into their set-theoretic or rather type-theoretic formulations.

From such a formalisation one can immediately derive an executable function nf. This function nf is given by type-theoretic code and executed by the normaliser of the implemented type theory. It may seem that nothing has been gained because one normalisation procedure has been implemented in terms of another one. Note, however, that the normal forms from Section 2.3 are a simple inductive definition so that in order to compute them one only needs iterative weak head reduction for closed terms on the meta-level.

A more efficient program can be obtained by translating the type-theoretic code into a functional program, for instance in Standard ML. To do this one has to systematically replace dependentlytyped inductive definitions by recursive datatypes and delete computationally-irrelevant arguments. For example the type of the semantic values which in the type-theoretic formulation depends on types and on (convertibility classes of) terms becomes in Standard ML the following recursive datatype where Tm is a simple inductive definition of terms.

datatype Sem = s_arr of int->Sem -> Sem |
               s_pi of int->((Sem -> Tm)*(Tm -> Sem)) -> Sem |
               s_u of Tm;

The integers are the “residuum” of the variable renamings in the type-theoretic formulation.

In order to justify these changes of data structure a general theory is called for. Lacking such theory at the moment we have to content ourselves with intuition and—if desired—a brute-force verification of the SML program using logical relations defining in which sense the SML program simulates the type-theoretic one. Having obtained such an SML program for normalisation of typetheoretic expression one has achieved the goal of employing the interpreter of the functional language for the purpose of normalisation although the interpreter itself performs weak-head reduction. Such an SML program exists and has been successfully tested on examples though has not been verified formally.

There are various ways in which the present work can be extended. A relatively easy task is the addition of inductive types such as a natural numbers type N with primitive recursion to F_{βη}. One has to adjust the definitions of normal forms and neutral terms and defines nat^{pred} as the property of being convertible to a normal form. The interpretation of zero and successor is then straightforward, for the interpretation of the recursor one uses primitve recursion over normal forms of N in 𝕍̂. Similarly, one can treat binary sum types albeit not with a general η-rule like in (Ghani 1995). Incorporating η-equality for sums constitutes a difficult problem and requires further research, yet we consider it an interesting task because usual term rewriting is not applicable to ηequality for sum types as it would violate Church-Rosser, a property irrelevant for the reduction-free approach.

The other direction consists of extending the present method to dependently typed systems. Although there are no principle obstacles this requires considerable effort because the notions of model involved are more complex. In view of the results in the present paper adding impredicativity would be a straightforward matter once type dependency has been settled. For a restricted notion of equality (namely equality of whnfs) this programme has already been carried out by Per Martin-Löf (1975). Using the ideas of higher-order abstract syntax and presheaf models we hope to be able to extend Martin-Löf’s result to full βη-equality.

References

Altenkirch, T., M. Hofmann, and T. Streicher (1995). Categorical reconstruction of a reductionfree normalisation proof. In D. Pitt and D. Rydeheard (Eds.), Proc. CTCS ’95, Springer LNCS, Vol. 953, pp. 182–199.

Altenkirch, T., M. Hofmann, and T. Streicher (1996). Reduction-free normalisation for a poly-

morphic system. In Proc. LICS ’96, New Brunswick, N. J. IEEE. Asperti, A. and S. Martini (1992). Categorical models of polymorphism. Information and Com-

putation 99, 1–79. Berger, U. and H. Schwichtenberg (1991). An inverse of the evaluation functional for typed λ-

calculus. In Proceedings of LICS ’91, Amsterdam, pp. 203–211. Burstall, R. and J. McKinna (1993). Deliverables: An approach to program semantics in con-

structions. In Proc. MFCS ’93, Springer LNCS, Vol. 711. Also as LFCS technical report ECS-LFCS-91-133.

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

Prentice-Hall. Coquand, C. (1994). From semantics to rules: a machine-assisted analysis. In Börger, Gurevich,

and Meinke (Eds.), Proceedings of CSL ’93, pp. 171–185. Springer, LNCS. Coquand, T. and P. Dybjer (1996). Intuitionistic model constructions and normalization proofs.

Mathematical Structures in Computer Science. To appear. Previous version has appeared in

the informal proceedings of the BRA-Types workshop, 1993 held in Nijmegen. Crole, R. (1993). Categories for Types. Cambridge University Press. Despeyroux, J., A. Felty, and A. Hirschowitz (1995). Higher-order abstract syntax in Coq. In

M. Dezani and G. Plotkin (Eds.), Typed Lambda Calculi and Applications, pp. 124–138. Springer LNCS vol. 902.

Ghani, N. (1995). βη-equality for coproducts. In Proceedings of TLCA ’95, Edinburgh. Springer.

LNCS 902. Harper, R., F. Honsell, and G. Plotkin (1993, January). A framework for defining logics. Journal

of the ACM 40 (1), 143–184. Huet, G. (1976). Résolution d’équations dans des langages d’ordre 1, 2, …, ω. Ph. D. thesis,

Université de Paris VII. Jacobs, B. (1991). Categorical Type Theory. Ph. D. thesis, University of Nijmegen. Lambek, J. and P. Scott (1985). Introduction to Higher-Order Categorical Logic. Cambridge

University Press. 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. 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. Moerdijk, I. and S. M. Lane (1992). Sheaves in Geometry and Logic. A First Introduction to

Topos Theory. Springer. Phoa, W. (1992). An introduction to fibrations, topos theory, the effective topos, and modest

sets. Technical Report ECS-LFCS-92-208, LFCS Edinburgh. Streicher, T. (1991). Semantics of Type Theory. Birkhäuser.