Categorical Logic

A chapter in the forthcoming Volume VI of Handbook of Logic in Computer Science

S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds), Oxford University Press

Andrew M. Pitts

Cambridge University Computer Laboratory

Cambridge CB2 3QG, UK ⟨ap@cl.cam.ac.uk⟩

18 May 1995

Categorical Logic

Andrew M. Pitts

Contents

1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2 Equational Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2.1 Syntactic Considerations . . . . . . . . . . . . . . . . . . 6 2.2 Categorical Semantics . . . . . . . . . . . . . . . . . . . . 7 2.3 Internal Languages . . . . . . . . . . . . . . . . . . . . . 10

3 Categorical Datatypes . . . . . . . . . . . . . . . . . . . . . . . 12 3.1 Disjoint union types . . . . . . . . . . . . . . . . . . . . . 14 3.2 Product types . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3 Function types . . . . . . . . . . . . . . . . . . . . . . . . 22 3.4 Inductive types . . . . . . . . . . . . . . . . . . . . . . . 24 3.5 Computation types . . . . . . . . . . . . . . . . . . . . . 27

4 Theories as Categories . . . . . . . . . . . . . . . . . . . . . . . 29 4.1 Change of category . . . . . . . . . . . . . . . . . . . . . 29 4.2 Classifying category of a theory . . . . . . . . . . . . . . 30 4.3 Theory-category correspondence . . . . . . . . . . . . . . 35 4.4 Theories with datatypes . . . . . . . . . . . . . . . . . . 37

5 Predicate Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5.1 Formulas and sequents . . . . . . . . . . . . . . . . . . . 39 5.2 Hyperdoctrines . . . . . . . . . . . . . . . . . . . . . . . 40 5.3 Satisfaction . . . . . . . . . . . . . . . . . . . . . . . . . . 44 5.4 Propositional connectives . . . . . . . . . . . . . . . . . . 46 5.5 Quantification . . . . . . . . . . . . . . . . . . . . . . . . 51 5.6 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 5.7 Completeness . . . . . . . . . . . . . . . . . . . . . . . . 59

6 Dependent Types . . . . . . . . . . . . . . . . . . . . . . . . . 62 6.1 Syntactic considerations . . . . . . . . . . . . . . . . . . 63 6.2 Classifying category of a theory . . . . . . . . . . . . . . 69 6.3 Type-categories . . . . . . . . . . . . . . . . . . . . . . . 71 6.4 Categorical semantics . . . . . . . . . . . . . . . . . . . . 76 6.5 Dependent products . . . . . . . . . . . . . . . . . . . . . 81

7 Further Reading . . . . . . . . . . . . . . . . . . . . . . . . . . 85

1 Introduction

This chapter provides an introduction to the interaction between category theory and mathematical logic. Category theory describes properties of mathematical structures via their transformations, or ‘morphisms’. On the other hand, mathematical logic provides languages for formalizing properties of structures directly in terms of their constituent parts—elements of sets, functions between sets, relations on sets, and so on. It might seem that the kind of properties that can be described purely in terms of morphisms and their composition would be quite limited. However, beginning with the attempt of Lawvere [1964, 1966, 1969, 1970] to reformulate the foundations of mathematics using the language of category theory the development of categorical logic over the last three decades has shown that this is far from true. Indeed it turns out that many logical constructs can be characterized in terms of relatively few categorical ones, principal among which is the concept of adjoint functor. In this chapter we will see such categorical characterizations for, amongst other things, the notions of variable, substitution, propositional connectives and quantifiers, equality, and various type-theoretic constructs. We assume that the reader is familiar with some of the basic notions of category theory, such as functor, natural transformation, (co)limit, and adjunction: see Poigné’s chapter on Basic Category Theory in Vol. I of this handbook, or any of the several introductions to category theory slanted towards computer science which now exist, such as [Barr and Wells, 1990], [Pierce, 1991].

Overview

There are three recurrent themes in the material we present.

Categorical semantics. Many systems of logic can only be modelled in a sufficiently complete way by going beyond the usual, set-based structures of classical model theory. Categorical logic introduces the idea of a structure valued in a category C, with the classical model-theoretic notion of structure [Chang and Keisler, 1973] appearing as the special case when C is the category of sets and functions. For a particular logical concept, one seeks to identify what properties (or extra structure) are needed in an arbitrary category to interpret the concept in a way that respects given logical axioms and rules. A well-known example is the interpretation of simply typed lambda calculus in cartesian closed categories (see Section 3.3).

Such categorical semantics can provide a completely general and often quite simple formulation of what is required to model (a theory in) the logic. This has proved useful in cases where more traditional, set-theoretic methods of defining a notion of model either lack generality, or are inconveniently complicated to describe, or both. Seely’s [1987] modelling of various impredicative type theories, such as the Girard-Reynolds polymorphic lambda calculus [Girard, 1986], [Reynolds, 1983] is an example of this: see [Reynolds and Plotkin, 1993] and [Pitts, 1987, 1989] for instances of the use of categorical models in this case.

Internal languages. Category theory has evolved a characteristic form of proof by ‘diagram-chasing’ to establish properties expressible in category theoretic terms. In complex cases, such arguments can be difficult to construct and hard to follow, because of the rather limited forms of expression of purely category-theoretic language. Categorical logic enables the use of richer (and more familiar) forms of expression for establishing properties of particular kinds of category. One first defines a suitable ‘internal language’ naming the relevant constituents of the category and then applies a categorical semantics to turn assertions in a suitable logic over the internal language into corresponding categorical statements. Such a procedure has become most highly developed in the theory of toposes, where the internal language of a topos, coupled with the semantics of intuitionistic higher order logic in toposes, enables one to reason about the objects and morphisms of a topos ‘as though they were sets and functions’ (provided one reasons constructively): see [Mac Lane and Moerdijk, 1992, VI.5], [Bell, 1988], or [McLarty, 1992, Chp. 14]. This technique has been particularly helpful for working with toposes that contain ‘sets’ that have properties incompatible with classical logic: cases in point are the modelling of the untyped lambda calculus in terms of objects that retract onto their own function space by D. Scott [1980], and the Moggi-Hyland modelling of the Girard-Reynolds polymorphic lambda calculus by an internal full subcategory of the effective topos of Hyland [1988].

Term-model constructions. In many cases, the categorical semantics of a particular kind of logic provides the basis for a correspondence between formal theories in the logic and instances of the appropriate kind of category. In one direction, the correspondence associates to such a category the theory induced by its internal language. In the other direction one has to give a ‘term-model’ construction manufacturing an instance of the required categorical structure out of the syntax of the theory. An example of such a correspondence is that between theories in βη-equational logic over simply typed lambda calculus and cartesian closed categories. Another example is the correspondence between theories in extensional higher order intuitionistic logic and toposes. These are both examples in which a variety of category theory was discovered to correspond to a pre-existing type of logic, with interesting consequences for both sides of the equation. On the other hand, some varieties of category, embodying important mathematical constructs, have required the invention of new types of logic to establish such a theory–category correspondence. A prime example of this is the notion of category with finite limits (variously termed a cartesian, or a lex category), for which a number of different logics have been devised: the essentially algebraic theories of Freyd [1972], the lim-theories of Coste [1979, Section 2], and the generalized algebraic theories of Cartmell (see Section 6) can all be used for this purpose, although each has its drawbacks.

Categories arising from theories via term-model constructions can usually be characterized up to equivalence by a suitable universal property (cf. Theorem 4.2.5, for example). This has enabled meta-theoretic properties of logics to be proved via categorical algebra. For example, Freyd’s proof of the existence and disjunction properties in intuitionistic logic is a case in point (see [Freyd and Scedrov, 1990, Appendix B.32]). It makes use of a categorical construction variously called sconing, or glueing. The same construction was used by Lafont to prove a strong conservativity result for the simply typed lambda calculus generated by an algebraic theory: see [Crole, 1993, Section 4.10]. A categorical construction closely related to glueing was used in [Crole and Pitts, 1992] to prove an existence property for a logic for fixed point recursion. One of the strengths of the categorical approach to logic is that the same categorical construction can sometimes be applied to obtain results for a number of different logics.

Contents of this chapter

We will not attempt a complete survey of all aspects of categorical logic that have been used, or might be used, in computer science applications. The author doubts that this can be done within the confines of a single chapter whilst avoiding superficiality. Instead we present a basic core of material in some detail.

Section 1 explains the categorical semantics of many-sorted equational logic in a category with finite products. Although the material involved is quite straightforward, we treat it carefully and in some detail since it provides the foundation for what we do in the rest of the chapter. Even at this simple level some important general features emerge—such as the role of finite products for modelling terms with several variables (independently of the presence of product types in the logic). Section 2 considers the categorical semantics of some simple type constructors. We attempt to demonstrate that the necessary categorical structure for a particular type constructor can be derived from its introduction, elimination and equality rules in a systematic way, given the basic framework of Section 2—a ‘doit-yourself categorical logic’, to echo the title of [Backhouse et al., 1989]. Then in Section 4 we consider a term-model construction for equational logic (with or without simple types) and the resulting theory–category correspondence.

The rest of the chapter builds on this material in two, orthogonal directions. In Section 5 we consider the categorical semantics of first order predicate logic, using a version of Lawvere’s ‘hyperdoctrines’. In Section 6 we present the author’s distillation of several related approaches to equational logic with dependent types. Finally, Section 7 gives pointers to the literature on aspects of categorical logic not treated here.

2 Equational Logic

It has proved useful in many situations to generalize the usual notion of algebraic structure by endowing the carrier set (or sets, in the many-sorted case) with some extra mathematical structure and insisting that the operations of the algebra preserve that structure. An example from the realm of programming semantics is the use of algebras whose carriers are domains and whose operations are continuous—see [Goguen et al., 1977]. Organizing the relevant mathematical structures and structure-preserving functions into a category C, algebras with such extra structure can be viewed as a natural generalization of the usual notion of algebra: instead of using algebras valued in the category Set of sets and functions, one is using algebras valued in the particular category C. To make sense of this notion for a general category, it is sufficient that it possess finite products. To motivate the interpretation of algebraic structure at this level of generality, let us see how to recast the usual, set-based semantics in a way that emphasises functions between sets rather than elements of sets.

Suppose then that we are given a many-sorted signature Sg, consisting of some sort symbols, σ, and some typed function symbols

F : σ_{1}, …, σ_{n} ⟶ τ .

Fixing disjoint, countably infinite sets of variables for each sort symbol, the (open) terms over Sg and their sorts are defined in the usual way: if x is a variable of sort σ, then x is a term of sort σ; and if F : σ_{1}, …, σ_{n} ⟶ τ is a function symbol and M_{1}, …, M_{n} are terms of sorts σ_{1}, …, σ_{n} respectively, then F (M_{1}, …, M_{n}) is a term of sort σ. (In case n = 0, F is just a constant and we abbreviate F () to F.) We will write M : σ to indicate that M is a term of sort σ.

Recall that a set-valued structure for Sg is specified by giving a set [[σ]] for each sort symbol σ and a function [[F]] : [[σ_{1}]] × ⋯ × [[σ_{n}]] ⟶ [[τ]] for each function symbol F : σ_{1}, …, σ_{n} ⟶ τ. The set [[σ_{1}]] × ⋯ × [[σ_{n}]] is the cartesian product of the sets [[σ_{i}]] and so consists of n-tuples (a_{1}, …, a_{n}) with a_{i} ∈ [[σ_{i}]]. In the case n = 0, this cartesian product contains just one element, the 0-tuple (), and so specifying the function [[F]] amounts to picking a particular element of [[σ]].

Given such a structure for Sg, the usual environment-style semantics for terms is defined by structural induction:

[[x]]ρ =^{def} ρ(x)
[[F (M_{1}, …, M_{n})]]ρ =^{def} [[F]]([[M_{1}]]ρ, …, [[M_{n}]]ρ)

where the ‘environment’ ρ is a finite partial function assigning elements of the structure to variables (respecting their sorts). Then an equation between two terms, M = N, is satisfied by the structure if for all environments defined on the variables occurring in M and N, [[M]]ρ and [[N]]ρ are equal elements of the structure

This explanation of the meaning of terms and equations is couched in terms of elements of sets. However, we can reformulate it in terms of functions between sets and using only category-theoretic properties of Set. This reformulation will allow us to replace the category Set of sets and functions by other suitable categories. First note that for any fixed list of distinct variables [x : σ_{1}, …, x_{n} : σ_{n}], the set of environments defined just on this set of variables is in bijection with the cartesian product [[σ_{1}]] × ⋯ × [[σ_{n}]]. Then the mapping ρ ↦ [[M]]ρ determines a function [[σ_{1}]]×⋯×[[σ_{n}]] ⟶ [[τ]] (assuming M has sort τ) which captures the meaning of the term M in the structure. In particular, the satisfaction of an equation amounts to the equality of the corresponding functions. So we can get a semantics expressed via functions rather than elements if we give meaning not to a naked term, but rather to a ‘term-in-context’, that is, to a term together with a list of distinct variables containing at least those which actually occur in the term. This also allows us to drop the syntactic convention that occurrences of variables in terms be explicitly typed, by recording the sort of a variable just once, in the context. The next section summarizes this approach to the syntax.

2.1 Syntactic Considerations

Suppose given a many-sorted signature Sg as above and a fixed, countably infinite set of variables, Var.

Definition 2.1.1. A context, Γ, is a finite list [x_{1} : σ_{1}, …, x_{n} : σ_{n}] of (variable, sort)-pairs, subject to the condition that x_{1}, …, x_{n} are distinct; we will write var(Γ) for the finite set {x_{1}, …, x_{n}} of variables in Γ. We will write Γ, x : σ to indicate the result of extending Γ by assigning the sort σ to a variable x ∉ var(Γ); similarly, the result of appending two contexts whose sets of variables are disjoint will be indicated by Γ, Γ′.

A term-in-context takes the form

M : σ [Γ]  (2.1)

where M is a term, σ is a sort, and Γ is a context over the given signature Sg. The well-formed terms-in-context are inductively generated by the two rules

x : σ [Γ, x : σ, Γ′]  (2.2)

{M_{1} : σ_{1} [Γ] ⋯ M_{n} : σ_{n} [Γ] \atop F (M_{1}, …, M_{n}) : τ [Γ]}  (2.3)

M = M : σ [Γ]  (2.6)

{M = M′ : σ [Γ] \atop M′ = M : σ [Γ]}  (2.7)

{M = M′ : σ [Γ] M′ = M′′ : σ [Γ] \atop M = M′′ : σ [Γ]}  (2.8)

{M = M′ : σ [Γ] N = N′ : τ [Γ, x : σ, Γ′] \atop N[M/x] = N′[M′/x] : τ [Γ, Γ′]}  (2.9)

Fig. 1. Equational Logic

where in (2.3), F : σ_{1}, …, σ_{n} ⟶ τ is any function symbol in the given signature.

A rule for substitution is derivable from rules (2.2) and (2.3):

{M : σ [Γ] N : τ [Γ, x : σ, Γ′] \atop (N[M/x]) : τ [Γ, Γ′]}  (2.4)

where N[M/x] denotes the result of substituting M for x in N. A rule for weakening contexts is a special case of (2.4):

{M : σ [Γ] \atop M : σ [Γ, Γ′]} .  (2.5)

An equation-in-context takes the form M = M′ : σ [Γ] where Γ is a context, σ is a sort and M, M′ are terms satisfying M : σ [Γ] and M′ : σ [Γ]. We will consider a (many-sorted) algebraic theory, Th, to consist of a signature Sg together with a collection of equations-in-context over Sg, called the axioms of Th. The theorems of Th are the equations-in-context over Sg that are provable from the axioms of Th using the rules of equational logic. These rules are shown in Fig. 1.

2.2 Categorical Semantics

Throughout this section C will be a fixed category with finite products. The product of a finite list [X_{1}, …, X_{n}] of objects in C will be denoted by X_{1} × ⋯ × X_{n}, with product projection morphisms

π_{j} : X_{1} × ⋯ × X_{n} ⟶ X_{j}.

Given morphisms f_{i} : Y ⟶ X_{i},

⟨f_{1}, …, f_{n}⟩ : Y ⟶ X_{1} × ⋯ × X_{n}

will denote the unique morphism whose compositions with each π_{i} is f_{i}. For definiteness we will assume that the product X_{1} × ⋯ × X_{n} is defined by induction on the length of the list [X_{1}, …, X_{n}] using a terminal object, 1, and binary products, − × −. Thus the product of the empty list is 1; and, inductively, the product of a list [X_{1}, …, X_{n}, X_{n+1}] of length n + 1 is given by the binary product (X_{1} × ⋯ × X_{n}) × X_{n+1}.

A structure in C for a given signature Sg is specified by giving an object [[σ]] in C for each sort σ, and a morphism [[F]] : [[σ_{1}]] × ⋯ × [[σ_{n}]] ⟶ [[τ]] in C for each function symbol F : σ_{1}, …, σ_{n} ⟶ τ. (In case n = 0, this means that a structure assigns a global element [[c]] : 1 ⟶ [[τ]] to a constant c : τ.) Given such a structure, for each context Γ = x_{1} : σ_{1}, …, x_{n} : σ_{n}, term M and sort τ for which M : τ [Γ] holds, we will define a morphism in C:

[[M : τ[Γ]]] : [[Γ]] ⟶ [[τ]]

where [[Γ]] denotes the product [[σ_{1}]] × ⋯ × [[σ_{n}]]. Note that the rules for deriving well-formed terms-in-context are such that for each Γ, M and τ, there is at most one way to derive M : τ[Γ]. The definition of [[M : τ[Γ]]] can therefore be given by induction on the structure of this derivation. Since it is also the case that τ is uniquely determined by Γ and M, we will abbreviate [[M : τ[Γ]]] to [[M[Γ]]]. The definition has two clauses, corresponding to rules (2.2) and (2.3):

[[x_{i}[x_{1} : σ_{1}, …, x_{n} : σ_{n}]]] =^{def} π_{i}
[[F (M_{1}, …, M_{n})[Γ]]] =^{def} [[F]] ∘ ⟨[[M_{1}[Γ]]], … [[M_{n}[Γ]]]⟩

Lemma 2.2.1 (Semantics of substitution). In the categorical semantics of terms-in-context, substitution of a term for a variable in a term is interpreted via composition in the category. Specifically, if M_{i} : σ_{i} [Γ′] for i = 1, …, n, and if N : τ [Γ] with Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}], then

[[(N[M⃗/x⃗])[Γ′]]] = [[N[Γ]]] ∘ ⟨[[M_{1}[Γ′]]], …, [[M_{n}[Γ′]]]⟩

where N[M⃗/x⃗] denotes the result of simultaneously substituting M_{i} for x_{i} (i = 1, …, n) in N. (Note that (N[M⃗/x⃗]) : τ [Γ′] holds by repeated use of (2.4).)

The lemma is proved by induction on the structure of N. By taking the terms M_{i} to be suitable variables one obtains the following result as a special case.

Corollary 2.2.2 (Semantics of weakening). Suppose that N : τ [Γ] and that Γ′ is another context that contains Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}] as a sub-list. Then [[N[Γ′]]] = [[N[Γ]]] ∘ π, where π = ⟨π_{m(1)}, …, π_{m(n)}⟩ with m(i) the position in Γ′ of the variable x_{i}.

Suppose M = M′ : σ [Γ] is an equation-in-context over a given signature, Sg. Since M : σ [Γ] and M : σ [Γ] are required to hold, a structure in C for Sg gives rise via the above definition, to morphisms [[M[Γ]]], [[M′[Γ]]] : [[Γ]] ⟶ [[σ]]. The structure is said to satisfy the equationin-context if these morphisms are equal. If Th is an algebraic theory over Sg, then the structure is a Th-algebra in C if it satisfies all the axioms of Th. There are very many different categories with finite products, and algebras for an algebraic theory in one may have very different detailed structure from algebras for the same theory in another category. Nevertheless, the following proposition shows that whatever the underlying category, we can still use the familiar kind of equational reasoning embodied by the rules in Fig. 1 whilst preserving satisfaction of equations.

Theorem 2.2.3 (Soundness). Let C be a category with finite products and Th an algebraic theory. Then a Th-algebra in C satisfies any equationin-context which is a theorem of Th.

Proof. The properties of equality of morphisms in C imply that the collection of equations-in-context satisfied by the Th-algebra is closed under rules (2.6), (2.7) and (2.8) in Fig. 1. Closure under rule (2.9) is a consequence of Lemma 2.2.1.

The converse of this theorem, namely the completeness of the categorical semantics for equational logic, will be a consequence of the material in Section 4.2.

Summary. We conclude this section by summarizing the important features of the categorical semantics of terms and equations in a category with finite products.

• Sorts are interpreted as objects.

• A term is only interpreted in a context (an assignment of sorts to finitely many variables) containing at least the variables mentioned in the term, and such a term-in-context is interpreted as a morphism with:

∗ the codomain of the morphism determined by the sort of the term;

∗ the domain of the morphism determined by the context;

∗ variables interpreted as product projection morphisms (identity morphisms being a special case of these);

∗ substitution of terms for variables interpreted via composition and pairing;

∗ weakening of contexts interpreted via composition with a prod-

uct projection morphism.

• An equation is only considered in a context (containing at least the variables mentioned), and such an equation-in-context is satisfied if the two morphisms interpreting the equated terms-in-context are actually equal in the category.

2.3 Internal Languages

The interpretation of equational logic described in the the previous section provides a means of describing certain properties of a category C with finite products as though its objects were sets of elements and its morphisms functions between those sets. To do this we use the terms over a manysorted signature Sg_{C} naming the objects and morphisms of C. The sorts of Sg_{C} are the objects of C; and for each non-empty list X_{1}, …, X_{n}, Y of objects, the function symbols of type X_{1}, …, X_{n} ⟶ Y are the morphisms f : X_{1}×⋯×X_{n} ⟶ Y in C. Of course the size of this signature depends on the size of C: it will have a set of symbols rather than a proper class, only if C is small (i.e. has only a set of morphisms). For the sake of clarity, we are not making a notational distinction between a symbol in Sg_{C} and the element of C that it names; as a result a morphism f : X_{1} ×⋯×X_{n} ⟶ Y occurs in Sg_{C} both as an n-ary function symbol of type X_{1}, …, X_{n} ⟶ Y and as a unary one of type X_{1} × ⋯ × X_{n} ⟶ Y.

The terms-in-context over this signature constitute a language for describing morphisms of C—a so-called internal language for C . The connection between these terms-in-context and the morphisms they describe is given by means of the evident structure for Sg_{C} in C which maps symbols in Sg_{C} to the corresponding objects and morphisms in C. Given M : Y [x_{1} : X_{1}, …, x_{n} : X_{n}], the definitions of Section 2.2 applied to this structure yield a morphism

[[M[x_{1} : X_{1}, …, x_{n} : X_{n}]]] : X_{1} × ⋯ × X_{n} ⟶ Y

in C.

We will not refer to this structure for Sg_{C} in C by name, but simply say that ‘C satisfies M = N : X [Γ]’ if the structure satisfies this equation-in-context. The following results are easy exercises in the use of the categorical semantics.

Proposition 2.3.1.

(i) Two parallel morphisms in C, f, g : X ⟶ X, are equal if and only if C satisfies f(x) = g(x) : X [x : X].

(ii) A morphism f : X ⟶ X in C is the identity on X if and only if C

satisfies f(x) = x : X [x : X]. (iii) A morphism f : X ⟶ Z is the composition of g : X ⟶ Y and

h : Y ⟶ Z if and only if C satisfies f(x) = h(g(x)) : Z [x : X]. (iv) An object T is a terminal object in C if and only if there is some

morphism t : 1 ⟶ T satisfying x = t : T [x : T].

(v) X ⟵^{p} Z ⟶^{q} Y is a binary product diagram in C if and only if there is some morphism r : X × Y ⟶ Z satisfying

p(r(x, y)) = x : X [x : X, y : Y]
q(r(x, y)) = y : Y [x : X, y : Y]
r(p(z), q(z)) = z : Z [z : Z].

The internal language of C makes it look like a category of sets and functions: given an object X, its ‘elements’ in the language are the terms M of sort X; and a morphism f : X ⟶ Y yields a function sending ‘elements’ M of sort X to ‘elements’ f(M) of sort Y. However, in the internal language the ‘elements’ of X depend upon the context; and these elements are interpreted as morphisms to X in C whose domain is the interpretation of the context. Thus we can think of morphisms x : I ⟶ X in C as generalized elements of X at stage I and will write x ∈_{I} X to indicate this.

A particular case is when I is the terminal object 1: the generalized elements of an object at stage 1 are more normally called its global elements. In general, it is not sufficient to restrict attention to global elements in order to describe properties of C. For example, each morphism f : X ⟶ Y yields via composition a function taking generalized elements of X at each stage I, x ∈_{I} X, to generalized elements of Y at the same stage, (f ∘ x) ∈_{I} Y. Two such morphisms f, g : X ⟶ Y are equal just in case they determine equal functions on generalized elements at all stages, but are not necessarily equal if they determine the same functions just on global elements. Call a category with terminal object well-pointed if for all f, g : X ⟶ Y in C, f = g whenever f ∘ x = g ∘ x for all global elements x : 1 ⟶ X. Typically, categories of sets equipped with extra structure and structure-preserving functions are well-pointed, and algebraic structures in such categories are closely related to corresponding set-valued structures via the use of global elements. If we only consider algebras in such well-pointed categories, we lose the ability to model certain phenomena. Here is a little example stolen from [Goguen and Meseguer, 1985], to do with ‘empty sorts’.

Example 2.3.2. Consider the usual algebraic theory of boolean algebras (with sort bool and operations T, F, ≅, ∨, ¬) augmented with a second sort hegel and a function symbol C : hegel ⟶ bool satisfying the axiom ¬(C(x)) = C(x) : bool [x : hegel]. Then T = F : bool [x : hegel] is a theorem of this theory, but T = F : bool [] is not. Any set-valued model of the theory that assigns a non-empty set to hegel must identify T and F. However, there are models in non-well-pointed categories for which hegel is non-empty (in the sense of not being an initial object).

For example, consider the category [ω, Set] of set-valued functors and natural transformations from the ordinal ω (which is a poset, hence a category). A more concrete description of [ω, Set] is as the category of ‘sets evolving through (discrete) time’. The objects are sets X equipped with a function E : X ⟶ ω recording that x ∈ X exists at time E(x) ∈ ω, together with a function (−)^{+} : X ⟶ X describing how elements evolve from one instant to the next, and hence which is required to satisfy E(x^{+}) = E(x)+1. A morphism between two such objects, f : X ⟶ Y, is a function between the sets which preserves existence (E(f(x)) = E(x)) and evolution (f(x^{+}) = f(x)^{+}). The global sections of X are in bijection with the elements which exist at the beginning of time, {x ∈ X | E(x) = 0}. So this category is easily seen to not be well-pointed. One can model the algebraic theory of the previous paragraph in this category by interpreting bool as the set having two distinct elements at time 0 that evolve to a unique element at time 1, and interpreting hegel as the set with no elements at time 0 and a single element thereafter. (This interpretation for hegel is different from the initial object of [ω, Set], which has no elements at any time.)

The internal language of a category with just finite products is of rather limited usefulness, because of the very restricted forms of expression and judgement in equational logic. However, internal languages over richer logics can be used as powerful tools for proving complicated ‘arrow-theoretic’ results by more familiar looking ‘element-theoretic’ arguments. See [Bell, 1988], for extended examples of this technique in the context of topos theory and higher order predicate logic. The use of categorical semantics in nonwell-pointed categories gives us an increase in ability to construct useful models compared with the more traditional ‘sets-and-elements’ approach. The work of Reynolds and Oles [1985] on the semantics of block structure using functor categories is an example. (As the example above shows, functor categories are not well-pointed in general.) See [Mitchell and Scott, 1989] for a comparison of the categorical and set-theoretic approaches in the case of the simply typed lambda calculus.

3 Categorical Datatypes

This section explores the categorical treatment of various type constructors. We postpone considering types that depend upon variables until section 6, and concentrate here upon ‘simple’ types with no such dependencies. We will consider properties of these types expressible within the realm of equational logic; so from the work in the previous section we know that at the categorical level we must start with a category with finite products and ask what more it should satisfy in order to model a particular type constructor. We hope to demonstrate that the necessary categorical structure for a particular type constructor can be derived from its introduction, elimination and equality rules in a systematic way, given the basic framework of the previous section.

In fact what emerges is an interplay between type theory and categorical structure. To model the term-forming operations associated with a type constructor one needs certain structures in a category; but then the characterization (up to isomorphism) of these structures via categorical properties (typically, adjointness properties) sometimes suggests extra, semantically meaningful rules to add to the logic.

Meta-linguistic conventions

The term-forming operations we will consider in this and subsequent sections will contain various forms of variable-binding, with associated notions of free and bound variables and substitution. To deal with all this in a uniform manner, we adopt a higher-order meta-language of ‘arities and expressions’ as advocated by Martin-Löf. See [Nordström et al., 1990, Chapter 3] for an extended discussion of this approach. For our purposes it is sufficient to take this meta-theory to be a simply typed lambda calculus with α-, β-, and η-conversion, whose terms will be called meta-expressions. The result of applying meta-expression e to meta-expression e′ will be denoted e(e′), with a repeated application such as e(e′)(e′′) abbreviated to e(e′, e′′); in certain situations the application e(e′) will be written e_{e′}. Lambda abstraction in the meta-language will be denoted (x)e, with a repeated lambda abstraction such as (x)(y)e abbreviated to (x, y)e. Equality of meta-expressions up to α-, β-, and η-conversion will be denoted e ≡ e′. Thus one has (x)e ≡ (y)(e[y/x]), ((x)e)(e′) ≡ e[e′/x] and (x)(e(x)) ≡ e.

The types of the meta-language will be called arities. For the moment we will assume that the arities are built up from two ground arities, Types and Terms, standing respectively for the syntactic categories of object language types and object language terms. Higher function arities will be indicated by Arity ↠ Arity′. So for example, Types ↠ Terms is the arity of functions assigning a term expression to each type expression. For a many-sorted signature, Sg, as in Section 2, we now regard the function symbols F of Sg are meta-constants of arity Terms^{n} ↠ Terms for various n, and regard the sorts as meta-constants of arity Types. The countably infinite set Var of variables used in that section will be identified with the metavariables of arity Terms.

Throughout this section we will assume that such a signature Sg has been given. On the category-theoretic side, C will denote a category with at least finite products, and we assume that a structure for Sg in C has been given. The simple types and their associated terms will be built up over the sorts of Sg. In this context, it is more usual to refer to the sorts of Sg as ground types. As before, terms and equations will only be considered in the presence of finite contexts assigning types to variables.

Remark 3.0.1 (Uniqueness of typing derivations and uniqueness of types). The various rules we will give for forming terms-in-context and equations-in-context are meant to augment the basic ones of equational logic given in Section 2 (i.e. (2.2), (2.4) and (2.6)–(2.4)). The new rules retain the property that there is at most one derivation of a typing judgement M : σ [Γ]. Thus the definition of its meaning as a morphism [[M[Γ]]] : [[Γ]] ⟶ [[σ]] in C can be given unambiguously by induction on the structure of this derivation. The same is true for the rules considered in Section 5. It is only when we come to consider dependent type theories in Section 6 that this property breaks down and a more careful approach to the categorical semantics must be adopted. We will also take care to retain the property of derivable typing judgements, M : σ [Γ], that σ is uniquely determined by the term M and the context Γ. This is the reason for the appearance of type subscripts in the syntax given below for the introduction terms of disjoint union, function and list types.

Remark 3.0.2 (Implicit contexts). In order to make the statement of rules less cluttered, from now on we will adopt the convention that a left-hand part of a context will not be shown if it is common to all the judgements in a rule. Thus for example rule (3.2) below is really an abbreviation for

C : σ + σ′ [Γ] N(x) : τ [Γ, x : σ] N′(x′) : τ [Γ, x′ : σ]
case(C, N, N′) : τ [Γ]

Remark 3.0.3 (Congruence rules). The introduction and elimination rules for the various datatype constructors to be given below have associated with them congruence rules expressing the fact that the term-forming constructions respect equality. For example, the congruence rules corresponding to (3.1) and (3.2) are:

{M_{1} = M_{2} : σ \atop inl_{σ′}(M_{1}) = inl_{σ′}(M_{2}) : σ + σ′}  {M′_{1} = M′_{2} : σ′ \atop inl_{σ}(M′_{1}) = inl_{σ}(M′_{2}) : σ + σ′}

C_{1} = C_{2} : σ + σ′ N_{1}(x) = N_{2}(x) : τ [x : σ] N′_{1}(x) = N′_{2}(x) : τ [x : σ] case(C_{1}, N_{1}, N′_{1}) = case(C_{2}, N_{2}, N_{2},) : τ .

We will not bother to give such congruence rules explicitly in what follows.

3.1 Disjoint union types

We will use infix notation and write σ + σ′ rather than +(σ, σ′) for the disjoint union of two types σ and σ′. (Thus this type constructor has arity Types ↠ Types ↠ Types.) The rules for introducing terms of type σ+σ′ are

{M : σ \atop inl_{σ′}(M) : σ + σ′}  {M′ : σ′ \atop inr_{σ}(M′) : σ + σ′}  (3.1)

and the corresponding elimination rule is

{C : σ + σ′ N(x) : τ [x : σ] N′(x′) : τ [x′ : σ] \atop case(C, N, N′) : τ}  (3.2)

What structure in a category C with finite products is needed to define [[M[Γ]]] in the presence of these new term-forming operations? We already have at our disposal the general framework for interpreting equational logic in categories with finite products, given in the previous section. Since this is our first example of the technique, we will proceed with some care in applying this framework.

Formation. Since types σ get interpreted as objects X = [[σ]] of C, we need a binary operation, X, X′ ↦ X + X′, on objects in order to interpret the formation of disjoint union types as:

[[σ + σ′]] =^{def} [[σ]] + [[σ′]]

Introduction. Since terms-in-context M : σ [Γ] get interpreted as morphisms from I = [[Γ]] to X = [[σ]], to interpret the introduction rules (3.1) we need functions on hom-sets of the form

C(I, X) ⟶ C(I, X + X′) C(I, X′) ⟶ C(I, X + X′)

that can be applied to [[M[Γ]]] and [[M′]][Γ] respectively to give the interpretation of inl_{σ′}(M) and inr_{σ}(M′). Now in the syntax, substitution commutes with term formation, and since substitution is interpreted by composition in C, it is necessary that the above functions be natural in I. Therefore by the Yoneda Lemma (see [Mac Lane, 1971, III.2]), there are morphisms X ⟶ X + X′ and X′ ⟶ X + X′ which induce the above functions on hom-sets via composition. So associated with the object X + X′ we need morphisms

inl_{X,X′} : X ⟶ X + X′ and inr_{X,X′} : X ⟶ X + X′

and can then define

[[inl_{σ′}(M)[Γ]]] =^{def} inl_{[[σ]],[[σ′]]} ∘ [[M[Γ]]]
[[inr_{σ}(M′)[Γ]]] =^{def} inr_{[[σ]],[[σ′]]} ∘ [[M[Γ]]]

Elimination. Turning now to the interpretation of the elimination rule (3.2), we need a ternary function on hom-sets of the form

case_{I} : C(I, X + X′) × C(I × X, Y) × C(I × X′, Y) ⟶ C(I, Y)

and as before, it must be natural in I because of the way that substitution is modelled by composition in C. Naturality here means that for each g : I′ ⟶ I

case_{I}(c, n, n′) ∘ g = case_{I′}(c ∘ g, n ∘ (g × id), n′ ∘ (g × id)).

Applying this with π_{2}, n ∘ (π_{1} × id), and n′ ∘ (π_{1} × id) for c, n, and n′ respectively, gives

case_{I}(c, n, n′) = case_{I×(X+X′)}(π_{2}, n ∘ (π_{1} × id), n′ ∘ (π_{1} × id)) ∘ ⟨id, c⟩

since π_{2}∘⟨id, c⟩ = c and (π_{1}×id)∘(⟨id, c⟩×id) = id. So in fact case_{I}(c, n, n′) can be expressed more fundamentally as a composition {n|n′}_{I} ∘ ⟨id, c⟩ where

{−|−}_{I} : C(I × X, Y) × C(I × X′, Y) ⟶ C(I × (X + X′), Y) (3.3)

is a family of functions, natural in I. Thus the semantics of case-terms becomes:

[[case(C, N, N′)[Γ]]] =^{def} {[[N(x)[Γ, x : σ]]]|[[N′(x′)[Γ, x′ : σ′]]]}_{[[Γ]]}∘⟨id, [[C[Γ]]]⟩.

Equality. Next we consider equality rules for σ + σ′. Consider first the familiar rules:

{M : σ N(x) : τ [x : σ] N′(x′) : τ [x′ : σ′] \atop case(inl_{σ′}(M), N, N′) = N(M) : τ}  (3.4)

{M′ : σ′ N(x) : τ [x : σ] N′(x′) : τ [x′ : σ′] \atop case(inr_{σ}(M′), N, N′) = N′(M′) : τ}  (3.5)

Writing m : I ⟶ X for [[M[Γ]]], m′ : I ⟶ X′ for [[M′[Γ]]], n : I ×X ⟶ Y for [[N(x)[Γ, x : σ]]] and n′ : I × X′ ⟶ Y for [[N′(x′)[Γ, x′ : σ′]]], then from above we have that [[case(inl_{σ′}(M), N, N′)[Γ]]] is {n|n′}_{I} ∘ ⟨id, inl_{X,X′} ∘ m⟩ and [[case(inr_{σ}(M), N, N′)[Γ]]] is {n|n′}_{I} ∘ ⟨id, inr_{X,X′} ∘ m⟩. From Lemma 2.2.1 giving the semantics of substitution, we also have that [[N(M)[Γ]]] is n ∘ ⟨id, m⟩ and that [[N(M′)[Γ]]] is n′ ∘ ⟨id, m⟩. Consequently the structure on C for interpreting terms associated with disjoint union types described above, is sound for the rules (3.4) and (3.5) provided the equations

{n|n′}_{I} ∘ ⟨id, inl_{X,X′} ∘ m⟩ = n ∘ ⟨id, m⟩
{n|n′}_{I} ∘ ⟨id, inr_{X,X′} ∘ m⟩ = n′ ∘ ⟨id, m⟩

hold for all m, n and n′ (with appropriate domains and codomains). Clearly for this it is sufficient to require for all n and n′ that

{n|n′}_{I} ∘ ⟨id, inl_{X,X′}⟩ = n  (3.6)

{n|n′}_{I} ∘ ⟨id, inr_{X,X′}⟩ = n′  (3.7)

and the naturality of {−|−}_{I} ensures that (3.6) and (3.7) are also necessary for the previous two equations to hold for all m, n and n′.

So we require that {−|−}_{−} provides a natural left inverse to the natural transformation

⟨(id × inl_{X,X′})^{∗}, (id × inr_{X,X′})^{∗}⟩ :
C(− × (X + X′), Y) ⟶ C(− × X, Y) × C(− × X′, Y) (3.8)

which sends f to (f ∘ (id × inl_{X,X′}), f ∘ (id × inr_{X,X′})). If furthermore, we require that it provide a two-sided inverse, so that

f = {f ∘ (id × inl_{X,X′})|f ∘ (id × inr_{X,X′})}_{I}  (3.9)

then the categorical semantics becomes sound for a further rule for σ + σ′, namely:

C : σ + σ′ F (z) : τ [z : σ + σ′]
case(C, (x)F (inl_{σ′}(x)), (x′)F (inr_{σ}(x′))) = F (C) : τ

(3.10)

(Recall that an expression like (x)F (inl_{σ′}(x)) denotes a lambda abstraction in the meta-language.)

If we think of (3.4) and (3.5) as the ‘β-rules’ for disjoint union, then (3.10) is an ‘η-rule’. As we will see, the rule is necessary if we wish σ + σ′ to be characterized up to isomorphism by σ and σ′.

Now taking the component of (3.8) at the terminal object 1 and using the canonical isomorphisms π_{2} : 1 × (−) ≅ (−), gives that

⟨inl_{X,X′}^{∗}, inr_{X,X′}^{∗}⟩ : C(X + X′, Y) ⟶ C(X, Y) × C(X′, Y)

is a bijection for each Y. By definition, this means that

X \underleftarrow{inl_{X,X′}} X + X′ \underrightarrow{inr_{X,X′}} X′

is a binary coproduct diagram in C. We will denote the inverse bijection to ⟨inl_{X,X′}^{∗}, inr_{X,X′}^{∗}⟩ at a pair of morphisms f : X ⟶ Y, f′ : X′ ⟶ Y by

( \begin{matrix}f \\ f′ \end{matrix} ) : X + X′ ⟶ Y.

So we are led to require that C have binary coproducts. But this is not all: we can now compose the the natural bijection (3.8) with

C(− × X, Y) × C(− × X′, Y) ≅ C((− × X) + (− × X′), Y)

to deduce that for each I, X, X′, composition with the canonical morphism

d =^{def} ( \begin{matrix}id × inl_{X,X′} \\ id × inr_{X,X′} \end{matrix} ) : (I × X) + (I × X′) ⟶ I × (X + X′) (3.11)

induces a bijection on hom-sets, and hence by the Yoneda Lemma, that d must be an isomorphism. In this case we say that binary products distribute over binary coproducts in C, or simply that C has stable binary coproducts. Thus the construct {−|−}_{−} takes n : I × X ⟶ Y and n′ : I × X′ ⟶ Y to

\{n|n′\}_{I} =^{def} ( \begin{matrix}n \\ n′ \end{matrix} ) ∘ d^{−1} : I × (X + X′) ⟶ Y

Defining satisfaction of equations-in-context over this richer collection of terms just as in Section 2.2, the Soundness Theorem 2.2.3 extends to include the equality rules for disjoint unions, i.e. if C is a category with finite products and stable binary coproducts, then the equations-in-context that are satisfied by a structure in C are closed under the rules of Equational Logic augmented by rules (3.4), (3.5) and (3.10). As with all categorical structure defined by universal properties, coproducts in a category are unique up to isomorphism. So we have that the structure needed in a category to interpret disjoint unions with all three equality rules is essentially unique. If we do not wish to model the third equality rule (3.10), then we have seen that a weaker structure than stable coproducts is sufficient—just inl_{X,X′}, inr_{X,X′} and an operation {−|−}_{−} satisfying the two equations (3.6) and (3.7), together with the naturality condition:

{n ∘ (g × id)|n′ ∘ (g × id)}_{I′} = {n|n′}_{I} ∘ (g × id).

(This naturality is automatic in the presence of the uniqueness rule (3.10).) However, in this case there may be several non-isomorphic ‘disjoint unions’ for X and X′ in C. Put another way, provided the third equality rule (3.10) is included, the rules for disjoint unions characterize this type constructor up to bijection. This kind of observation seems important from a foundational point of view, and arises very naturally from the categorical approach to logic.

The stability of binary coproducts in C says precisely that for each object I, the functor I × (−) : C ⟶ C preserves binary coproducts. Since coproducts, being colimits, are preserved by any functor with a right adjoint, stability is automatic if each I×(−) : C ⟶ C has a right adjoint. The value of this right adjoint at an object X is by definition the exponential object I→X. In particular if C is a cartesian closed category, then coproducts in C are automatically stable, since all exponential objects exist in this case by definition. We will see in Section 3.3 that exponential objects model function types. So if one is only concerned with modelling disjoint sums in a higher-order setting, one need only verify the presence of coproducts in the category. Here is an example of a category with non-stable coproducts (and hence without exponentials).

Example 3.1.1. Recall that the category of complete, atomic boolean algebras and boolean homomorphisms is equivalent to the opposite of the category of sets and functions. In Set one generally does not have

I + (X × X′) ≅ (I + X) × (I + X′) .

(Consider the case I = X = X′ = 1, for example.) Thus in the opposite of the category of sets, binary coproducts are not in general stable, and hence nor are they stable in the category of complete atomic boolean algebras. Therefore, even though this category has coproducts (it has all small limits and colimits), we cannot soundly interpret disjoint union types in it.

Remark 3.1.2 (Empty type). We have treated binary disjoint union types. The ‘nullary’ version of this is the empty type null, with rules:

C : null ; empty_{τ} (C) : τ
C : null F (z) : τ [z : null]
empty_{τ} (C) = F (C) : τ

These rules can be soundly interpreted in C if it has a stable initial object, 0 . This means that not only is 0 initial (i.e. for each object X, there is a unique morphism 0 ⟶ X), but so also is I × 0 for any object I. This latter condition is equivalent to requiring that π_{2} : I × 0 ⟶ 0 is an isomorphism. As before, this stability condition is automatic if the functors I × (−) : C ⟶ C have right adjoints, and thus in particular, an initial object in a cartesian closed category is automatically stable.

3.2 Product types

One could be forgiven for jumping straight to the conclusion that product types σ × σ′ should be interpreted by binary categorical product in a category C. However, as we have seen in Section 2, the finite product structure of C is there primarily to enable terms involving multiple variables to be interpreted. Also, we will use the elimination rule for products that is derived systematically from its formation and introduction rule, rather than the more familiar formulation in terms of first and second projection. (See [Backhouse et al., 1989] for comments on this issue in general.) Nevertheless, with a full set of equality rules including the analogue of the ‘surjective pairing’ rule, binary products in C are exactly what is required to model product types. If one does not wish to model the surjective pairing rule, then a weaker structure on C (not determined uniquely up to isomorphism) suffices.

Recall that the introduction rule and corresponding elimination rule for product types are

{M : σ M′ : σ′ \atop pair(M, M′) : σ × σ′}  (3.12)

{P : σ × σ′ N(x, x′) : τ [x : σ, x′ : σ′] \atop split(P, N) : τ}  (3.13)

(together with associated congruence rules—cf. Remark 3.0.3). By a similar analysis to that in Section 3.1, one finds that the following structure on C is needed to interpret these new terms:

• for all objects X, X′, an object X ∗ X′;

• for all objects X, X′, a morphism pair_{X,X′} : X × X′ ⟶ X ∗ X′;

• for all objects I, X, X′, Y, a function

split_{I} : C(I × X × X′, Y) ⟶ C(I × (X ∗ X′), Y)

that is natural in I (so that split_{I′}(n ∘ (g × id)) = split_{I}(n) ∘ (g × id) holds for all n : I × X × X′ ⟶ Y and g : I′ ⟶ I).

The semantics of product types and terms in C are then:

[[σ × σ′]] =^{def} [[σ]] ∗ [[σ′]]
[[pair(M, M′)[Γ]]] =^{def} pair_{[[σ]],[[σ′]]} ∘ ⟨[[M[Γ]]], [[M′[Γ]]]⟩
[[split(P, N)[Γ]]] =^{def} split_{[[Γ]]}([[N(x, x′)[Γ, x : σ, x′ : σ′]]]) ∘ ⟨id, [[P [Γ]]]⟩

The equality rules for product types are:

M : σ M′ : σ′ N(x, x′) : τ [x : σ, x′ : σ′]
split(pair(M, M′), N) = N(M, M′) : τ

(3.14)

P : σ × σ′ N(z) : τ [z : σ × σ′]
split(P, (x, x′)N(pair(x, x′))) = N(P) : τ

(3.15)

For the above semantics to be sound for (3.14), one needs that that for each n : I × X × X′ ⟶ Y in C

split_{I}(n) ∘ (id × pair_{X,X′}) = n.

In other words, the natural transformation induced by pre-composition with (id × pair_{X,X′})

(id × pair)_{X,X′}^{∗} : C(− × (X ∗ X′), Y) ⟶ C(− × X × X′, Y) (3.16)

should have left inverse given by n ↦ split_{I}(n). This condition does not suffice to determine X ∗ X′ uniquely up to isomorphism: there may be several different such ‘weak product’ structures on C. However, if we insist that (3.15) is also satisfied, i.e. that

split_{I}(n ∘ (id × pair_{X,X′})) = n,

then split_{−} becomes a two-sided inverse for (3.16). By considering the component of this natural isomorphism at the terminal object, one has that pre-composition with pair : X × X′ ⟶ X ∗ X′ induces a bijection on hom-sets, and hence is itself an isomorphism. Consequently to interpret product types satisfying both equality rules, the structure needed on C must be essentially the existing binary product structure (and so in particular, is unique up to isomorphism). Thus the semantics of product types and terms in C simplifies to:

[[σ × σ′]] =^{def} [[σ]] × [[σ′]]
[[pair(M, M′)[Γ]]] =^{def} ⟨[[M[Γ]]], [[M′[Γ]]]⟩
[[split(P, N)[Γ]]] =^{def} [[N(x, x′)[Γ, x : σ, x′ : σ′]]] ∘ ⟨id, [[P [Γ]]]⟩.

In particular, the definable first and second projections

fst(z) =^{def} split(z, (x, x′)x)
snd(z) =^{def} split(z, (x, x′)x′)

when interpreted give the first and second projection morphisms as one might hope:

[[fst(z)[z : σ × σ′]]] = π_{1} : [[σ]] × [[σ′]] ⟶ [[σ]]
[[snd(z)[z : σ × σ′]]] = π_{2} : [[σ]] × [[σ′]] ⟶ [[σ′]].

Remark 3.2.1 (One-element type). The ‘nullary’ version of binary product types is the one-element type unit with the following rules (together with associated congruence rules). As for product types, we use the possibly less familiar elimination rule derived systematically from the form of formation and introduction.

⋆ : unit

U : unit N : τ
proj(U, N) : τ
U : unit N(z) : τ [z : unit]
proj(U, N(⋆)) = N(U) : τ

The last rule is the analogue of rule (3.15)—in other words, it is the ‘η-rule’ for this type. The ‘β-rule’ for unit (analogous to (3.14)) is

{N : τ \atop proj(⋆, N) = N : τ}

but it is easy to see that in fact this rule is derivable from the above rules, as is the rule

U : unit ; U = ⋆ : unit

Using an argument similar to that for product types, one finds that these rules can be interpreted soundly in C provided it has a terminal object.

3.3 Function types

Since types σ get interpreted as objects X = [[σ]] of C, we need a binary operation, X, X′ ↦ X→X′, on objects in order to interpret function types σ→σ′ as follows:

[[σ→σ′]] =^{def} [[σ]]→[[σ′]]

Introduction. The introduction rule for function types is:

{F (x) : τ [x : σ] \atop λ_{σ}(F) : σ→τ} .  (3.17)

To interpret this rule in a category C with finite products we need a function on hom-sets of the form

cur_{I} : C(I × X, Y) ⟶ C(I, X→Y)

in order to define

[[λ_{σ}(F)[Γ]]] =^{def} cur_{[[Γ]]}([[F (x)[Γ, x : σ]]]).

In order to preserve the basic property of the semantics that substitution is modelled by composition, we require the above functions to be natural in I, meaning

cur_{I′}(f ∘ (g × id)) = cur_{I}(f) ∘ g

holds for all f : I × X ⟶ Y and g : I′ ⟶ I.

Elimination. We will use the familiar elimination rule involving application rather that the rule systematically derived from formation and introduction, which involves judgements with higher-order contexts (see [Nordström et al., 1990, Section 7.2]).

{M : σ→τ N : σ \atop ap(M, N) : τ}  (3.18)

To interpret this rule, we need a function on hom-sets of the form

C(I, X→Y) × C(I, X) ⟶ C(I, Y)

which is natural in I (in order to respect the semantics of substitution in terms of composition). Naturality in I of these functions implies that they are induced by a morphism

ap_{X,Y} : (X→Y) × X ⟶ Y

and we define

[[ap(M, N)[Γ]]] =^{def} ap_{[[σ]],[[σ′]]} ∘ ⟨[[M[Γ]]], [[N[Γ]]]⟩.

Equality. The rule of β-conversion is

{F (x) : τ [x : σ] N : σ \atop ap(λ_{σ}(F), N) = F (N) : τ}  (3.19)

The structure in C we have described for interpreting function types is sound for this rule provided

ap_{X,Y} ∘ ⟨cur_{I}(f), n⟩ = f ∘ ⟨id, n⟩

holds for all f : I × X ⟶ Y and n : I ⟶ X. For this it is sufficient, and because of the naturality of cur also necessary that

ap_{X,Y} ∘ (cur_{I}(f) × id) = f  (3.20)

hold for all f : I × X ⟶ Y.

The rule for η-conversion is

{M : σ→τ \atop λ_{σ}((x)ap(M, x)) = M : σ→τ}  (3.21)

The semantics is sound for this rule provided that for all m : I ⟶ (X→Y)

cur_{I}(ap_{X,Y} ∘ (m × id)) = m.  (3.22)

In fact the naturality of cur_{−} implies that this holds if and only if for each X and Y

cur_{I}(ap_{X,Y}) = id_{X→Y} .

Now (3.20) and (3.22) say precisely that the natural transformation

C(− × X, Y) ⟶ C(−, X→Y)

given by f ↦ ap_{X,Y} ∘ (f × id) is a bijection with inverse cur_{−}. Thus, by definition, X→Y is the exponential of Y by X in the category C, with evaluation morphism ap_{X,Y} : (X→Y) × X ⟶ Y. Recall that by definition, a cartesian closed category has all finite products and exponentials. Thus we have: function types satisfying β- and η-conversion can be soundly interpreted in C provided it is cartesian closed.

3.4 Inductive types

In this section we consider the categorical interpretation of inductively defined datatypes (such as the natural numbers, lists and trees) using initial algebras. For definiteness we will concentrate on the case of the list type constructor, σ ↦ σlist.

Recall that the introduction rules and corresponding elimination rule for σlist are:

nil_{σ} : σlist  M : σ L : σlist cons(M, L) : σlist  (3.23)

F (x, l, x′) : σ′ [x : σ, l : σlist, x′ : σ′] L : σlist M′ : σ′
listrec(F, L, M′) : σ′

(3.24)

By a process of analysis that one hopes is becoming familiar by now, one finds that the following structure on a category C with finite products is needed to interpret these new syntax.

• For each object X, an object LX equipped with morphisms nil_{X} : 1 ⟶ LX and cons_{X} : X × LX ⟶ LX.

• For all objects I, X, X′, an operation sending a morphism f : I ×X × LX × X′ ⟶ X′ to a morphism listrec_{I}(f) : I × LX × X′ ⟶ X′, which is natural in I (so that for all g : I′ ⟶ I, listrec_{I′}(f ∘ (g × id × id × id)) = listrec_{I}(f) ∘ (g × id × id)).

The semantics of σlist and its associated terms in C is then:

[[σlist]] =^{def} L[[σ]]
[[nil_{σ}[Γ]]] =^{def} nil_{[[σ]]} ∘ ⟨ ⟩_{L[[σ]]}
[[cons(M, L)[Γ]]] =^{def} cons_{[[σ]]} ∘ ⟨[[M[Γ]]], [[L[Γ]]]⟩
[[listrec(F, L, M′)[Γ]]] =^{def} listrec_{[[Γ]]}([[F (x, l, x′)[Γ, x : σ, l : σlist, x′ : σ′]]])
∘ ⟨id, [[L[Γ]]], [[M′[Γ]]]⟩.

(In the clause for nil_{σ}, ⟨ ⟩_{L[[σ]]} denotes the unique morphism from L[[σ]] to the terminal object 1.)

Now consider the usual equality rules for σlist:

F (x, l, x′) : σ′ [x : σ, l : σlist, x′ : σ′] M′ : σ′
listrec(F, nil_{σ}, M′) = M′ : σ′

(3.25)

F (x, l, x′) : σ′ [x : σ, l : σlist, x′ : σ′] M : σ L : σlist M′ : σ′

listrec(F, cons(M, L), M′) = F (M, L, listrec(F, L, M′)) : σ′

(3.26)

For the semantics to be sound for these two rules one needs that for each F : I × X × LX × X′ ⟶ X′ in C

listrec_{I}(f) ∘ ⟨π_{1}, nil_{X} ∘ ⟨ ⟩, π_{2}⟩ = π_{2} : I × X′ ⟶ X′  (3.27)

listrec_{I}(f) ∘ ⟨π_{1}, cons_{X} ∘ ⟨π_{2}, π_{3}⟩, π_{4}⟩ =
f ∘ ⟨π_{1}, π_{2}, π_{3}, listrec_{I}(f) ∘ ⟨π_{1}, π_{3}, π_{4}⟩⟩
: I × X × LX × X′ ⟶ X′  (3.28)

We can go one step further and insist that given f, listrec_{I}(f) is the unique morphism satisfying (3.27) and (3.28). In this case the structure on C is also sound for the rule

F (x, l, x′) : σ′ [x : σ, l : σlist, x′ : σ′]  L : σlist M′ : σ′ G(l, x′) : σ′ [l : σlist, x′ : σ′]  G(nil_{σ}, x′) = x′ : σ′ [x′ : σ′] G(cons(x, l), x′) = F (x, l, G(l, x′)) : σ′ [x : σ, l : σlist, x′ : σ′] G(L, M′) = listrec(F, L, M′) : σ′ .

(3.29)

With (3.29) and in the presence of product types, the scheme for primitive recursion becomes interdefinable with a simpler scheme of iteration, given by the following rules.

F (x, x′) : σ′ [x : σ, x′ : σ′] M′ : σ′
listit(F, M′, l) : σ′ [l : σlist]

(3.30)

F (x, x′) : σ′ [x : σ, x′ : σ′] M′ : σ′
listit(F, M′, nil_{σ}) = M′ : σ′

(3.31)

F (x, x′) : σ′ [x : σ, x′ : σ′] M′ : σ′

listit(F, M′, cons(x, l)) = F (x, listit(F, M′, l)) : σ′ [x : σ, l : σlist]

(3.32)

F (x, x′) : σ′ [x : σ, x′ : σ′]  M′ : σ′ G(l) : σ′ [l : σlist]  G(nil_{σ}) = M′ : σ′ G(cons(x, l)) = F (x, G(l)) : σ′ [x : σ, l : σlist] G(l) = listit(F, M′, l) : σ′ [l : σlist] .  (3.33)

For clearly iteration is a special case of primitive recursion, and in the reverse direction one can define

listrec(F, L, M′) =^{def} fst(listit((x, z)pair(F (x, fst(z), snd(z)), snd(z)), pair(nil_{σ}, M′), L))

and use (3.31), (3.32) and (3.33) to prove that this has the correct properties. To do this, one also has to prove that

snd(listit((x, z)pair(F (x, fst(z), snd(z)), snd(z)), pair(nil_{σ}, M′), L)) = L,

and this requires the uniqueness property (3.33).

In C, the rules (3.30–3.33) correspond to the following universal property of the object LX equipped with morphisms nil_{X} : 1 ⟶ LX and cons_{X} : X × LX ⟶ LX: for each pair of morphisms f : I × X × X′ ⟶ X′ and m′ : I ⟶ X′, there is a unique morphism g : I × LX ⟶ X′ such that the following diagrams commute:

[figure: I × 1; id_{I} × nil_{X}; I × LX; 1; π_{2}; m′; X′; g]

I × X × LX  \overline{\begin{matrix}id_{I×X} × cons_{X} \\  \end{matrix}}I × LX

[figure: I × X × X′; ⟨π_{1}, π_{2}, g ∘ ⟨π_{1}, π_{3}⟩⟩; f; X′; g]

The uniqueness property of g implies that the operation sending f to g is natural in I—so it is unnecessary to state this as a separate requirement. If the category C is cartesian closed, then a further simplification can be made: it is sufficient to have the above universal property for I = 1 to deduce the general case. If C also has binary coproducts, then one can combine nil_{X} and cons_{X} into a single morphism

i =^{def} ( \begin{matrix}nil & X \\ cons & X \end{matrix} ) : T (LX) ⟶ LX

where T : C ⟶ C is the functor 1+(X×−). The universal property enjoyed by nil_{X} and cons_{X} is equivalent to the following property of i: for each morphism h : T (X′) ⟶ X′, there is a unique morphism g : LX ⟶ X′ with g ∘ i = h ∘ T (g). In other words, (LX, i) is an initial object in the category of algebras for the functor T. (Recall that a T -algebra is an object X′ of C equipped with a ‘structure’ morphism T (X′) ⟶ X′; a morphism of T -algebras is a morphism in C between the underlying objects of the algebras that makes the evident square involving the structure morphisms commute.)

As usual, this initiality property characterizes LX, nil_{X} and cons_{X} uniquely up to isomorphism in C. Moreover, the structure morphism of an initial algebra is always an isomorphism: so i gives an isomorphism between 1 + (X × LX) and LX. (The inverse of i is the unique T -algebra morphism from the initial algebra to (T (LX), T (i)).)

Taking the type σ in σlist to be the one-element type unit, one obtains the type of natural numbers. On the categorical side, when X is the terminal object 1 in C, the above universal property of L1 is that given by Lawvere in defining the notion of a natural number object in a category. Other inductive datatypes (equipped with iterators satisfying uniqueness conditions) can be modelled soundly by requiring C to have initial algebras for the ‘strictly positive’ functors T : C ⟶ C—those expressible via a combination of constant functors, products, coproducts, and exponentiation by a fixed object.

Remark 3.4.1 (Weak natural numbers object). Without the uniqueness rules (3.29) or (3.33), the scheme of iteration is weaker than that of primitive recursion. (For example, the expected properties of the predecessor function on the natural numbers cannot be derived from an iterative definition—see [Girard, 1989, page 51].) The corresponding uniqueness part of the universal property defining the notion of natural number object N, makes this notion conditional-equational rather than equational. If this uniqueness requirement is removed, N is termed a weak natural numbers object. Lambek [1988] and Román [1989] have studied extensions of the algebraic theory of weak natural numbers involving Mal’cev operations in which the uniqueness of the iterator can be derived.

3.5 Computation types

Moggi [1991] introduces a new approach to the denotational semantics of programming languages based on the categorical notion of a strong monad and the corresponding type-theoretic notion of ‘computation types’. As a further illustration of the methods developed so far, we will give the semantics of Moggi’s ‘computational lambda calculus’ in a category with finite products equipped with a strong monad.

The syntax of computation types is as follows. We are given a unary type constructor σ ↦ T σ. One should think of T σ as the type of ‘computations’ of elements of type σ. There are two rules for building terms of computation types:

{M : σ \atop val(M) : T σ}  (3.34)

{E : T σ F (x) : T σ′ [x : σ] \atop let(E, F) : T σ′}  (3.35)

(together with associated congruence rules—cf. Remark 3.0.3).

Intuitively, val(M) is the value M regarded as a trivial computation which immediately evaluates to itself; and let(E, F) denotes the sequential computation which firstly tries to evaluate E to some value M : σ and then proceeds to evaluate F (M). These intended meanings motivate the following three equality rules:

{M : σ F (x) : T σ′ [x : σ] \atop let(val(M), F) = F (M) : T σ′}  (3.36)

{E : T σ \atop let(E, (x)val(x)) : T σ}  (3.37)

E : T σ F (x) : T σ′ [x : σ] G(x′) : T σ′′ [x′ : σ′] let(let(E, F), G) = let(E, (x)let(F (x), G)) : T σ′′ .  (3.38)

To interpret this syntax soundly in a category C with finite products we need the following structure on C:

• for each object X, an object TX

• for each object X, a morphism η_{X} : X ⟶ TX;

• for all objects I, X, X′, a function

lift_{I} : C(I × X, T(X′)) ⟶ C(I × TX, T(X′))

that is natural in I (so that lift_{I}(f) ∘ (g × id) = lift_{I′}(f ∘ (g × id)) holds for all f : I × X ⟶ T(X′) and g : I′ ⟶ I).

Then the semantics of computation types and their associated terms in C is:

[[T σ]] =^{def} T([[σ]])
[[val(M)[Γ]]] =^{def} η_{[[σ]]} ∘ [[M[Γ]]]
[[let(E, F)[Γ]]] =^{def} lift_{[[Γ]]}([[F (x)[Γ, x : σ]]]) ∘ ⟨id, [[E[Γ]]]⟩

Satisfaction of rules 3.36, 3.37 and 3.38 requires the following equational properties of η_{X} and lift_{I} to hold for all f : I × X ⟶ T(X′) and g :

I × T(X′) ⟶ T(X′′). (We have used the naturality of lift_{I} in I to state these in their simplest form.)

lift_{I}(f ∘ ⟨id, η_{X}⟩) = f
lift_{I}(η_{X} ∘ π_{1}) = π_{1} : I × X ⟶ X
lift_{I}(g) ∘ ⟨π_{1}, lift_{I}(f)⟩ = lift_{I}(lift_{I}(g) ∘ ⟨π_{1}, f⟩)

Specifying the structure (T, η, lift) with the above properties is in fact equivalent to specifying a monad on the category C together with a ‘tensorial strength’ for the monad: we refer the reader to [Moggi, 1991] and the references therein for more details. Note that unlike the other categorical datatypes considered in this section, for a given category C the structure of a strong monad is not determined up to isomorphism—there may be many different ones on C. (See loc. cit. for several examples with computational significance.)

4 Theories as Categories

Sections 2 and 3 have shown how to model an equational theory, possibly involving some simple datatypes, in a suitably structured category in a way which respects the rules of Equational Logic. The purpose of this section is to demonstrate that this categorical semantics is completely general, in the sense that the category theory provides an alternative, but equivalent formulation of the concepts embodied in the logic. We will see that there is a correspondence between theories and categories, which enables one to view the latter as giving an abstract, or presentation-free notion of theory.

Such a theory–category correspondence relies upon the fact that the categorical formulation of semantics allows us to consider models of a theory in different categories. For a given theory Th, amongst all these different categories it is possible to construct one which contains the ‘most general’ model of Th. This category is called the ‘classifying category’ of Th and the model it contains is called the ‘generic’ model. They are characterized by a certain category-theoretic, universal property which depends upon the ability to compare algebras in different categories by transporting them along functors preserving the relevant categorical structure. So we begin by describing this process.

Until Section 4.4 we will confine our attention to algebraic theories versus categories with finite products. Th will denote a fixed, many-sorted algebraic theory (as defined in Section 2.1), with underlying signature Sg.

4.1 Change of category

Recall that a functor T : C ⟶ D is said to preserve the finite product X_{1} × ⋯ × X_{n} if the morphisms T (π_{i}) : T (X_{1} × ⋯ × X_{n}) ⟶ T (X_{i}) make T (X_{1} × ⋯ × X_{n}) into the product of the T (X_{i}) in D. If D itself has finite products, then this is equivalent to requiring that

a =^{def} ⟨T (π_{1}), …, T (π_{n})⟩ : T (X_{1} × ⋯ × X_{n}) ⟶ T (X_{1}) × ⋯ × T (X_{n})

be an isomorphism. (A stronger condition would be to demand that a be an identity morphism—in which case we say that T strictly preserves the finite product X_{1} × ⋯ × X_{n}.)

If C and D are categories with finite products and T : C ⟶ D is a functor preserving them, then every structure S for Sg in C gives rise to a structure T (S) in D defined as follows:

T (S)[[σ]] =^{def} T (S[[σ]])
T (S)[[F]] =^{def} T (S[[F]]) ∘ a^{−1} .

for all sorts σ and function symbols F : σ_{1}, …, σ_{n} ⟶ τ. Since T preserves finite products and the semantics of terms-in-context is defined in terms of these, the meaning of a term in S is mapped by T to its meaning in T (S). More precisely, if M : τ [Γ] then

\begin{matrix}T (S)[[Γ]] & ≅^{a^{−1}} & T (S[[Γ]]) \\ T (S)[[τ]]^{T (S)[[M[Γ]]]} & = & T (S[[τ]])^{T (S[[M[Γ]]])} \end{matrix}

commutes in D. Consequently, if S satisfies M = M′ : τ [Γ], then so does T (S). Thus finite product preserving functors preserve the satisfaction of equations. In particular, if S is an algebra in C for a theory Th, then T (S) is an algebra for Th in D.

Example 4.1.1. If C is locally small, then for each object I in C the hom-functor C(I, ) : C ⟶ Set preserves products (but not strictly so, in general). Thus every algebra S in C gives rise to an ordinary, set-valued algebra C(I, S), whose elements are the ‘generalized elements of S at stage I’ in the sense of Section 2.3.

4.2 Classifying category of a theory

Two contexts over the signature Sg are α-equivalent if they differ only in their variables; in other words, the list of sorts occurring in each context are equal (and in particular, the contexts are of equal length). Clearly this gives an equivalence relation on the collection of contexts and the set of α-equivalence classes of contexts is in bijection with the set of lists of sorts in Sg. Assuming a fixed enumeration Var = {v_{1}, v_{2}, …} of the set of variables (i.e. of the set of meta-variables of arity Terms), we can pick a canonical representative context [v_{1} : σ_{1}, …, v_{n} : σ_{n}] for the α-equivalence class corresponding to each list σ_{1}, …, σ_{n} of sorts. We will not distinguish notationally between a context and the α-equivalence class it determines.

Given contexts Γ and Γ′ = [y_{1} : τ_{1}, …, y_{n} : τ_{m}], a context morphism from Γ to Γ′

γ : Γ ⟶ Γ′

is specified by a list γ = [N_{1}, …, N_{m}] of terms over Sg such that N_{j} : τ_{j} [Γ] holds for each j = 1, …, m. Note that Γ′ could be replaced by any αequivalent context without affecting this definition.

Given another such morphism γ′ = [N′_{1}, …, N′_{m}], we will write

γ =_{Th} γ′ : Γ ⟶ Γ′

to indicate the judgement that γ and γ′ are context morphisms from Γ to Γ′ that are Th-provably equal: by definition, this means that for each j = 1, …, m, N_{j} = N′_{j} : τ [Γ] is a theorem of Th. Rules (2.6), (2.7) and (2.8) imply that Th-provable equality of context morphisms (between two given contexts) is an equivalence relation. Moreover, rule (2.9) shows that changing Γ up to α-equivalence will not change the class of γ under this equivalence relation.

The composition of context morphisms γ : Γ ⟶ Γ′ and γ′ : Γ′ ⟶ Γ′′ is the context morphism γ′ ∘ γ : Γ ⟶ Γ′′ formed by making substitutions:

γ′ ∘ γ =^{def} [M_{1}[N⃗/y⃗], …, M_{n}[N⃗/y⃗]]

when Γ′ = [y_{1} : τ_{1}, …, y_{n} : τ_{m}], γ = [N_{1}, …, N_{m}] and γ′ = [M_{1}, …, M_{n}]. The fact that γ′ ∘ γ does constitute a context morphism from Γ to Γ′′ follows from rule (2.4); and rule (2.9) implies that composition respects Th-provable equality:

γ_{1} =_{Th} γ_{2} : Γ ⟶ Γ′ γ′_{1} =_{Th} γ′_{2} : Γ′ ⟶ Γ′′ γ′_{1} ∘ γ_{1} =_{Th} γ′_{2} ∘ γ_{2} : Γ ⟶ Γ′′ .

The usual properties of term substitution imply that composition of context morphisms is associative:

γ′′ ∘ (γ′ ∘ γ) =_{Th} (γ′′ ∘ γ′) ∘ γ : Γ ⟶ Γ′′′

when γ : Γ ⟶ Γ′, γ′ : Γ′ ⟶ Γ′′ and γ′′ : Γ′′ ⟶ Γ′′′. Moreover, the operations of composition possess units: the identity context morphism for Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}],

id_{Γ} : Γ ⟶ Γ

is given by the list id_{Γ} = [x_{1}, …, x_{n}] of variables in Γ; clearly one has

γ ∘ id_{Γ} =_{Th} γ : Γ ⟶ Γ′
id_{Γ′} ∘ γ =_{Th} γ : Γ ⟶ Γ′ .

We now have all the ingredients necessary to define a category. Specifically, the classifying category, Cℓ(Th), of an algebraic theory Th is defined as follows.

Objects of Cℓ(Th) are α-equivalence classes of contexts (or, if you prefer, finite lists of sorts) over the signature of Th.

Morphisms of Cℓ(Th) from one object Γ to another Γ′ are equivalence classes of context morphisms for the equivalence relation which identifies γ : Γ ⟶ Γ′ with γ′ : Γ ⟶ Γ′ just in case γ =_{Th} γ′ : Γ ⟶ Γ′. Composition of morphisms in Cℓ(Th) is induced by composition of context morphisms and identities are equivalence classes of identity context morphisms. We will not distinguish notationally between a context morphism and the morphism of Cℓ(Th) which it determines.

Proposition 4.2.1. Cℓ(Th) has finite products.

Proof. Clearly, for each context Γ the empty list of terms is the unique context morphism Γ ⟶ [ ], and so its equivalence class is the unique morphism from Γ to [ ] in Cℓ(Th). Thus the (α-equivalence class of the) empty context [ ] is a terminal object in Cℓ(Th).

Given contexts Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}] and Γ′ = [y_{1} : τ_{1}, …, y_{m} : τ_{m}], we make use of the given enumeration Var = {v_{1}, v_{2}, …} of the set of variables to define a context

Γ × Γ′ =^{def} [v_{1} : σ_{1}, …, v_{n} : σ_{n}, v_{n+1} : τ_{1}, …, v_{n+m} : τ_{m}]

Then [v_{1}, …, v_{n}] and [v_{n+1}, …, v_{n+m}] determine morphisms π_{1} : Γ×Γ′ ⟶ Γ and π_{2} : Γ × Γ′ ⟶ Γ′ in Cℓ(Th) which make Γ × Γ′ into the product of Γ and Γ′ in Cℓ(Th). For if γ = [M_{1}, …, M_{n}] : Δ ⟶ Γ and γ′ = [N_{1}, …, N_{m}] : Δ ⟶ Γ′ then [M_{1}, …, M_{n}, N_{1}, …, N_{m}] determines a context morphism ⟨γ, γ′⟩ : Δ ⟶ Γ × Γ′ which is unique up to Thprovability with the property that π_{1} ∘ ⟨γ, γ′⟩ = γ and π_{2} ∘ ⟨γ, γ′⟩ = γ′.

Remark 4.2.2. We could have defined Cℓ(Th) by taking its objects to be just contexts rather than α-equivalence classes of contexts; this would have resulted in a larger category, equivalent to the one defined above (and hence with the same categorical properties). One advantage of the definition we gave is that the particular choice of finite products given in the proof of Proposition 4.2.1 is strictly associative and strictly unital: this means that for all objects Γ, Γ′ and Γ′′, the morphisms

⟨⟨π_{1}, π_{1} ∘ π_{2}⟩, π_{2} ∘ π_{2}⟩ : Γ × (Γ′ × Γ′′) ⟶ (Γ × Γ′) × Γ′′
π_{1} : Γ × 1 ⟶ Γ
π_{2} : 1 × Γ ⟶ Γ

are not merely isomorphisms (as is always the case), but actually identity morphisms.

Remark 4.2.3. There is a close relationship between Cℓ(Th) and the free Th-algebras in Set generated by finitely many indeterminates. Writing Γ for [x_{1} : σ_{1}, …, x_{n} : σ_{n}], let F_{Th}(Γ) denote the free algebra generated by finitely many indeterminates x_{1}, …, x_{n} of sorts σ_{1}, …, σ_{n} respectively. Then F_{Th}(Γ) can be constructed by taking its underlying set at a sort τ to consist of the set of terms M satisfying M : τ [Γ], quotiented by the equivalence relation which identifies M with M′ just in case M = M′ : τ [Γ] is a theorem of Th. This quotient set is precisely the set of morphisms Γ ⟶ [v_{1} : τ] in Cℓ(Th). Thus the hom-sets of Cℓ(Th) can be used to construct the free finitely generated Th-algebras in Set. Conversely, it can be shown that the category Cℓ(Th) is equivalent to the opposite of the category whose objects are the free, finitely generated Th-algebras in Set, and whose morphisms are all Th-algebra homomorphisms.

Next we describe the ‘generic’ model of Th in the classifying category. Each sort σ of the underlying signature Sg of the theory Th determines determines an object in the classifying category of Th represented by the context [v_{1} : σ]. We will denote this object of Cℓ(Th) by G[[σ]]. If F : σ_{1}, …, σ_{n} ⟶ τ is a function symbol in Sg, then since

F (v_{1}, …, v_{n}) : τ [v_{1} : σ_{1}, …, v_{n} : σ_{n}]

we have that [F (v_{1}, …, v_{n})] is a context morphism from [v_{1} : σ_{1}, …, v_{n} : σ_{n}] to [v_{1} : τ]. Now the proof of Proposition 4.2.1 shows that in Cℓ(Th) the object [v_{1} : σ_{1}, …, v_{n} : σ_{n}] is the product of the objects [v_{i} : σ_{i}] = G[[σ_{i}]]; hence [F (v_{1}, …, v_{n})] determines a morphism G[[F]] : G[[σ_{1}]] × ⋯ × G[[σ_{n}]] ⟶ G[[τ]] in Cℓ(Th). Altogether then, G is a structure for Sg in the category Cℓ(Th).

Lemma 4.2.4. The structure G has the following properties.

(i) For each context Γ, the object G[[Γ]] in Cℓ(Th) is (the α-equivalence class of) Γ;

(ii) If M : τ [Γ] then the morphism G[[M[Γ]]] : G[[Γ]] ⟶ G[[τ]] in Cℓ(Th)

is that determined by the context morphism [M] : Γ ⟶ [v_{1} : τ]; (iii) M = M′ : τ [Γ] is a theorem of Th if and only if G[[M[Γ]]] =

G[[M′[Γ]]]. In other words, G satisfies an equation-in-context just

in case it is a theorem of Th.

Proof. (i) We have already observed that [v_{1} : σ_{1}, …, v_{n} : σ_{n}] is the product G[[σ_{1}]] × ⋯ × G[[σ_{n}]] in Cℓ(Th); but recall from Section 2.2 that this is also the definition of G[[[v_{1} : σ_{1}, …, v_{n} : σ_{n}]]].

(ii) This follows by induction on the structure of M using the explicit description of the product structure of Cℓ(Th) given in the proof of Proposition 4.2.1.

(iii) By part (ii), G[[M[Γ]]] = G[[M′[Γ]]] holds if and only if [M] and [M′] determine equal morphisms in Cℓ(Th), which by definition means that M = M′ : τ [Γ] is a theorem of Th.

Part (ii) of the above lemma implies in particular that G satisfies the axioms of Th and hence is a Th-algebra. G will be called the generic T h-algebra. It enjoys the following universal property.

Theorem 4.2.5 (Universal property of the generic algebra). For each category C with finite products, any Th-algebra S in C is equal to \overline{S}(G) for some finite product preserving functor \overline{S} : Cℓ(Th) ⟶ C. Moreover, the functor \overline{S} is uniquely determined up to (unique) natural isomorphism by the algebra S. (\overline{S} is called the functor classifying the algebra S.)

Proof. Define \overline{S} on objects Γ by

\overline{S}(Γ) =^{def} S[[Γ]]

and on morphisms γ = [N_{1}, …, N_{m}] : Γ ⟶ Γ′ by

\overline{S}(γ) =^{def} ⟨S[[N_{1}[Γ]]], …, S[[N_{m}[Γ]]]⟩ : S[[Γ]] ⟶ S[[Γ′]]

Then the fact that \overline{S} is a functor preserving finite products follows easily from the definition of Cℓ(Th) in Section 4.2. Applying \overline{S} to G, one has for a sort σ that \overline{S}(G)σ = \overline{S}(G[[σ]]) = S[[[v_{1} : σ]]] = S[[σ]], and similarly for a function symbol F that \overline{S}(G)F = \overline{S}(G[[F]]) = S[[F]]. Hence \overline{S}(G) = S.

Now suppose that T : Cℓ(Th) ⟶ C is another product-preserving functor and that there is an isomorphism, h : T (G) ≅ S, of Th-algebras in C. For each object Γ = [v_{1} : σ_{1}, …, v_{n} : σ_{n}] in Cℓ(Th), since Γ ≅ G[[σ_{1}]] × ⋯ × G[[σ_{n}]], one gets isomorphisms

T (Γ) ≅ T (G[[σ_{1}]] × ⋯ × G[[σ_{n}]])
≅ T (G)[[σ_{1}]] × ⋯ × T (G)[[σ_{n}]]
≅ S[[σ_{1}]] × ⋯ × S[[σ_{n}]]
=^{def} \overline{S}(Γ)

which are the components of a natural isomorphism k : T ≅ \overline{S}. Finally, note that since T and \overline{S} preserve finite products and every object in Cℓ(Th) is a finite product of objects of the form G[[σ]], k is uniquely determined by the condition that it induces h.

Corollary 4.2.6.

(i) The classifying category of Th is determined uniquely up to equivalence, and the generic Th-algebra uniquely up to isomorphism by the universal property in Theorem 4.2.5.

(ii) The operation of evaluating a finite product preserving functor from Cℓ(Th) to C at the generic algebra G is the object part of an equivalence of categories:

FP(Cℓ(Th), C) ≃ Th-ALG(C)  (4.1)

where FP(Cℓ(Th), C) is the category of finite product preserving functors and natural transformations from Cℓ(Th) to C, and Th-ALG(C) is the category of Th-algebras and homomorphisms in C.

Proof. Part (i) is a routine consequence of the universal property, but part (ii) deserves further comment.

The statement of Theorem 4.2.5 says that the functor T ↦ T (G) is essentially surjective, and full and faithful for isomorphisms; hence it gives an equivalence between the category of functors and natural isomorphisms and the category of algebras and algebra isomorphisms. Since this is true for any C with finite products, we can replace C by its arrow category C^{·→·} (whose objects are the morphisms of C and whose morphisms are commutative squares in C), which certainly has finite products when C does. The equivalence for objects and isomorphisms in this case implies that the original functor T ↦ T (G) is full and faithful, and hence that (4.1) holds.

4.3 Theory-category correspondence

Let Sg_{C} be the signature defined from a category C with finite products, as in Section 2.3. As we noted in that section, there is a canonical structure for Sg_{C} in C. Define Th_{C} to be the algebraic theory over Sg_{C} whose axioms are all equations-in-context which are satisfied by this structure. Then the structure is automatically an algebra for this theory, and hence by Theorem 4.2.5 corresponds to a finite product preserving functor T : Cℓ(Th_{C}) ⟶ C. The definition of Sg_{C} (which names the various objects and morphisms in C) and Th_{C} (which identifies terms which name the same things in C) entails that T is full, faithful and essentially surjective—and hence is an equivalence of categories. Thus we have that every category with finite products is equivalent to the classifying category of some manysorted algebraic theory. As we noted in Section 2.3, Th_{C} will have a set of symbols and axioms (rather than a proper class of them) only in the case that C is a small category.

Starting with C, forming Th_{C} and then Cℓ(Th_{C}) one obtains back not C itself, but an equivalent category. What about the reverse process: how are the theories Th and Th_{Cℓ(Th)} related? To answer this question, we need an appropriate notion of morphism, or translation between algebraic theories. A rather general notion is obtained by declaring a translation Th ⟶ Th′ to be an algebra for Th in the classifying category of Th′. The syntactic nature of the construction of Cℓ(Th′) permits one to give a purely syntactic explanation of this notion of translation, which we omit here. In fact we can form a 2-category of many-sorted algebraic theories, Alg, whose homcategories are the categories of algebras and homomorphisms in classifying categories:

Alg(Th, Th′) =^{def} Th-Alg(Cℓ(Th′)) .

If Fp denotes the 2-category whose objects are categories with finite products and whose hom-categories consist of finite product preserving functors and all natural transformations, then the classifying-category construction is the object part of a 2-functor

Cℓ : Alg ⟶ Fp .

This 2-functor is ‘full and faithful’ in the sense that it is an equivalence on hom-categories (using (4.1)), and is ‘essentially surjective’ in the sense that every object of Fp is equivalent to one in the image of Cℓ. Thus Cℓ induces an equivalence between Alg and Fp in an appropriate, up-to-equivalence sense.

Remarks 4.3.1. We close this section by mentioning some consequences of the correspondence.

(i) We can view a particular small category with finite products C as specifying a (many-sorted) algebraic theory independently of any particular presentation in terms of a signature and axioms: there may be many such presentations whose syntactic details are different, but which nevertheless specify the ‘same’ theory, in the sense that their classifying categories are equivalent to the given category C. Indeed, once one has this categorical view of algebraic theories, one sees that there are many ‘naturally occurring’ algebraic theories which do not arise in terms of a presentation with operators and equations. For example, the category whose objects are the finite cartesian powers of the set of natural numbers ℕ and whose morphisms ℕ^{m} ⟶ ℕ^{n} are ntuples of m-ary primitive recursive functions, is a category with finite products and hence an algebraic theory. This category is a paradigmatic example of the notion of ‘iteration theory’ introduced by Elgot: see the book by Bloom and Esik [1993]. (A reader who takes this advice should be warned that [Bloom and Ésik, 1993] adopts a not uncommon viewpoint that algebraic theories can be identified with categories with finite coproducts. Since the 2-category of categories with finite coproducts and functors preserving such is equivalent (under the 2-functor taking a category to its opposite category) to the 2-category of categories with finite products, this viewpoint is formally equivalent to the one presented here. However it does not sit well with the intuitively appealing picture we have built up of the sorts of a theory (objects of a category) as generalized sets and the terms-in-context (morphisms) as generalized functions.)

(ii) If T : C ⟶ D is a morphism in Fp between small categories, then for any C ∈ Fp with small colimits, it can be shown that the functor T^{∗} : Fp(D, C) ⟶ Fp(C, C) induced by composition with T has a left adjoint, given by left Kan extension along T. Since T corresponds to a translation between algebraic theories and T^{∗} is the functor restricting algebras along T, this left adjoint provides ‘relatively free’ constructions on algebras for a wide variety of situations (depending upon the nature of the translation).

(iii) Free constructions (indeed weighted colimits in general) in Fp can be constructed via appropriate syntactic constructions on algebraic theories and translations between them.

4.4 Theories with datatypes

In this section we will examine the effect on the classifying category Cℓ(Th) of a theory Th when we enrich equational logic with the various datatype constructions considered in Section 3, together with their associated introduction, elimination and equality rules. We will look at product, disjoint union and function types. In each case the classifying category turns out to possess the categorical structure that was used in Section 3 to interpret these datatype constructs. (Similar considerations apply to the other type forming operations considered in that section, namely list types and ‘computation’ types.)

Product types. (Cf. Section 3.2.) In this case, for each pair of types σ and σ′ there is a binary product diagram in the classifying category Cℓ(Th) of the form

[figure: [x : σ]; [fst(z)]; [z : σ × σ′]; [snd(z)]; [x′ : σ′] .]

Similarly, in the presence of a one-element type unit (cf. Remark 3.2.1), then [z : unit] is a terminal object in Cℓ(Th). It follows that in the presence of these type-forming constructs, Cℓ(Th) is equivalent to the full subcategory whose objects are represented by contexts of length one.

Disjoint union types. (Cf. Section 3.1.) In this case, for each pair of types σ and σ′ and each context Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}], there is a coproduct diagram in the classifying category Cℓ(Th) of the form

[figure: [Γ, x : σ]; [x⃗, inl_{σ′}(x)]; [Γ, z : σ + σ′]; [x⃗, inr_{σ}(x′)]; [Γ, x′ : σ′]]

(where x, x′, z are chosen to be distinct from x⃗ = x_{1}, …, x_{n}). In case Γ = ∅, we have that [z : σ + σ′] is the binary coproduct of [x : σ] and [x : σ] in Cℓ(Th). Given the description of products in the category Cℓ(Th) in Proposition 4.2.1, it also follows that product with an arbitrary object [Γ] distributes over this coproduct, i.e. it is a stable coproduct(cf. 3.1). Similarly, in the presence of an empty type (cf. Remark 3.1.2), [z : null] is a stable initial object in Cℓ(Th).

In the presence of product and one-element types we have seen that every object is isomorphic to one of the form [x : σ]. In this case the presence of disjoint union and empty types, we can conclude that Cℓ(Th) has all stable finite coproducts.

Function types. (Cf. Section 3.3.) In this case, for each pair of types σ and σ′, the object [f : σ→σ′] is the exponential of [x′ : σ′] by [x : σ] in Cℓ(Th), with associated evaluation morphism

[f : σ→σ′] × [x : σ] = [f : σ→σ′, x : σ] \overline{\begin{matrix}[ap(f, x)] \\  \end{matrix}}[x′ : σ′] .

Unlike the case for disjoint union types, it is not necessary to assume the presence of product types in order to conclude that the classifying category possesses exponentials for any pair of objects. For, given any objects Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}] and Γ′ = [x′_{1} : σ′_{1}, …, x′_{n} : σ′_{m}], the exponential [Γ]→[Γ′] in Cℓ(Th) is given by the object

[f_{1} : σ⃗→σ′_{1}, …, f_{m} : σ⃗→σ′_{m}]

where for each i = 1, …, m

σ⃗→σ′_{i} =^{def} σ_{1}→(σ_{2}→ ⋯ (σ_{n}→σ′_{i}) ⋯) .

Thus in the presence of function types, the classifying category Cℓ(Th) is a cartesian closed category, whether or not we assume the theory Th involves product types.

Remark 4.4.1 (The generic model of a theory). Suppose we consider equational theories Th in the equational logic of product, disjoint union and function types. We have seen that Cℓ(Th) is a cartesian closed category with finite coproducts. (Recall that the stability of coproducts is automatic in the presence of exponentials.) Such a category is sometimes called bicartesian closed. We can define a structure G in Cℓ(Th) for the underlying signature of Th just as in Section 4.2 and satisfying Lemma 4.2.4. Thus the structure G in Cℓ(Th) is a model of Th (i.e. satisfies the axioms of Th) and indeed satisfies exactly the equations that are theorems of Th. An immediate corollary of this property is the completeness of the categorical semantics: A equation is derivable from the axioms of Th using the equational logic of product, disjoint union and function types if (and only if) it is satisfied by all models of Th in bicartesian closed categories.

Indeed, Theorem 4.2.5 extends to yield a universal property characterizing G as the generic model of Th in bicartesian closed categories: given any other model S of Th in a bicartesian closed category C, then the functor \overline{S} : Cℓ(Th) ⟶ C defined in the proof of Theorem 4.2.5 is a morphism of bicartesian closed categories, i.e. preserves finite products, finite coproducts and exponentials. It also maps G to S and is unique up to unique isomorphisms with these properties.

5 Predicate Logic

In previous sections we have considered the categorical interpretation of properties of structures that can be expressed equationally. Now we consider what it means for a structure in a category to satisfy properties expressible in the (first order) predicate calculus, using logical connectives and quantifiers. As in section 3, adjunctions play an important role: we will see that the propositional connectives, the quantifiers, and equality can be characterized in terms of their adjointness properties. First we set up the basic framework of predicate logic and its categorical semantics.

5.1 Formulas and sequents

Let us augment the notion of many-sorted signature considered in section 2 by allowing not only sort and function symbols, but also relation symbols, R. We assume that each relation symbol comes equipped with a typing of the form R ⊆ σ_{1}, …, σ_{n}, indicating both the number and the sorts of the terms to which R can be applied. To judgements of the form 2.1 asserting that an expression is a well-formed term of a given sort in a given context, we add judgements of the form

ϕ prop [Γ]

asserting that the expression ϕ is a well-formed formula in context Γ. The atomic formulas over the given signature are introduced by the rules

M_{1} : σ_{1} [Γ] ⋯ M_{n} : σ_{n} [Γ]
\overline{(where R ⊆ σ_{1}, …, σ_{n})}
R(M_{1}, …, M_{n}) prop [Γ]

(5.1) with one such rule for each relation symbol R. Later we will consider compound formulas built up from the atomic ones using various proposition forming operations. The logical properties of these operations will be specified in terms of sequents of the form

Φ ⊢ ψ [Γ]  (5.2)

where Φ = ϕ_{1}, …, ϕ_{n} is a finite list of formulas, ψ is a formula and the judgements ϕ_{i} prop [Γ] and ψ prop [Γ] are derivable. The intended meaning of the sequent (5.2) is that the joint validity of all the formulas in Φ logically entails the validity of the formula ψ.

Fig. 2 gives the basic, structural rules for deriving sequents. Since we wish to consider predicate logic as an extension of the rules for equational logic given in section 2.1, Fig. 2 includes a rule (Subst) permitting the substitution in a sequent of a term for a provably equal one. The rule (Weaken) allows for weakening of contexts. The other possible form of weakening is to add formulas to the left-hand side of a sequent:

{Φ ⊢ ψ \atop Φ, Φ′ ⊢ ψ}

This is derivable from the rules in Fig. 2 because of the form of rule (Id). Note that in stating these rules we continue to use the convention established in Remark 3.0.2 that the left-hand part of a context is not shown if it is common to all the judgements in a rule. Thus for example, the full form of rule (Subst) is really

{M = M′ : σ [Γ′] Φ(x) ⊢ ψ(x) [Γ′, x : σ, Γ] \atop Φ(M) ⊢ ψ(M′) [Γ′, Γ]}

Let us enrich the notion of theory used in section 2 by permitting the signature of the theory to contain typed relation symbols in addition to sorts and typed function symbols, and by permitting the axioms of the theory to be sequents as well as equations-in-context. The theorems of such a theory will now be those judgements that can be derived from the axioms using the rules in Figures 1 and 2 (together with the rules for the various rules for proposition-forming operations to be considered below, as appropriate).

5.2 Hyperdoctrines

If the judgement ϕ prop [x_{1} : σ_{1}, …, x_{n} : σ_{n}] over a given signature is derivable, then {x_{1}, …, x_{n}} contains the variables occurring in the formula ϕ. Intuitively such a formula ϕ describes a subset of the product of the sorts σ_{1}, …, σ_{n}. Indeed, suppose we are given a set-valued structure for

Φ, ψ, ψ ⊢ θ ; (Contract) ; Φ, ψ ⊢ θ Φ, ψ, ψ′, Φ′ ⊢ θ

(Exchange)

Φ, ψ′, ψ, Φ′ ⊢ θ

\begin{aligned}& (Id) \\ Φ, ψ ⊢ ψ \end{aligned}  Φ ⊢ ψ Φ′, ψ ⊢ ψ′ ; (Cut) ; Φ, Φ′ ⊢ ψ′

Φ ⊢ ψ ; (Weaken) ; Φ ⊢ ψ [Γ]

M = M′ : σ Φ(x) ⊢ ψ(x) [x : σ, Γ]

(Subst)

Φ(M) ⊢ ψ(M′) [Γ]

Fig. 2. Structural rules

the signature: such a structure assigns a set [[σ]] to each sort σ, a function [[F]] : [[σ_{1}]] × ⋯ × [[σ_{n}]] ⟶ [[τ]] to each function symbol F : σ_{1}, …, σ_{n} ⟶ τ and a subset [[R]] ⊆ [[σ_{1}]] × ⋯ × [[σ_{n}]] to each relation symbol R ⊆ σ_{1}, …, σ_{n}. Then each formula-in-context ϕ prop [x_{1} : σ_{1}, …, x_{n} : σ_{n}] gives rise to the subset of [[σ_{1}]] × ⋯ × [[σ_{n}]] consisting of those n-tuples (a_{1}, …, a_{n}) for which the sentence ϕ[a_{1}/x_{1}, …, a_{n}/x_{n}] is satisfied in the classical, Tarskian sense (see [Chang and Keisler, 1973, 1.3]). Our aim is to explain how this traditional notion of satisfaction can be generalized to give an interpretation of formulas-in-context in categories other than the category of sets. To do this one needs a categorical treatment of the notion of ‘subset’ and the various operations performed on subsets when interpreting logical connectives and quantifiers. For this we will use the ‘hyperdoctrine’ approach originated by Lawvere [1969, 1970], whereby the ‘subsets’ of an object are given abstractly via additional structure on a category.

Definition 5.2.1. A prop-category, C, is a category possessing finite products and equipped with the following structure:

• For each object X in C, a partially ordered set Prop_{C}(X), whose elements will be called C-properties of X. The partial order on Prop_{C}(X) will be denoted by ≤.

• For each morphism f : Y ⟶ X in C, an operation assigning to each C-property A of X, a C-property f^{∗}A of Y called the pullback of A along f. These operations are required to be

monotone: if A ≤ A′, then f^{∗}A ≤ f^{∗}A′;

functorial: id^{∗}A = A and g^{∗}(f^{∗}A) = (f ∘ g)^{∗}A.

Thus a prop-category is nothing other than a category with finite products, C, together with a contravariant functor Prop_{C}(−) from C to the category of posets and monotone functions. Prop_{C}(−) is a particular instance of a Lawvere ‘hyperdoctrine’, which in general is category- rather than posetvalued (and pseudofunctorial rather than functorial). The reader should be warned that the term ‘prop-category’ is not standard; indeed there is no standard terminology for the various kinds of hyperdoctrine which have been used in categorical logic.

Here are some important examples of prop-categories from the worlds of set theory, domain theory and recursion theory.

Example 5.2.2 (Subsets). The category Set of sets and functions supports the structure of a prop-category in an obvious way by taking the Set-properties of a set X to be the ordinary subsets of X. Given a function f : Y ⟶ X, the operation f^{∗} is that of inverse-image, taking a subset A ⊆ X to the subset {y | f(y) ∈ A} ⊆ Y.

Example 5.2.3 (Inclusive subsets of cpos). Let Cpo denote the category whose objects are posets possessing joins of all ω-chains and whose morphisms are the ω-continuous functions (i.e. monotone functions preserving joins of ω-chains). This category has products, created by the forgetful functor to Set. We make it into a prop-category by taking Prop_{Cpo}(X) to consist of all inclusive subsets of X, i.e. those that are closed under joins of ω-chains in X. The partial order on Prop_{Cpo}(X) is inclusion of subsets. Given f : Y ⟶ X, since f is ω-continuous, the inverse image of an inclusive subset of X along f is an inclusive subset of Y; this defines the operation f^{∗} : Prop_{Cpo}(X) ⟶ Prop_{Cpo}(Y).

Example 5.2.4 (Realizability). The prop-category Kℓ has as underlying category the category of sets and functions. For each set X, the poset Prop_{Kℓ}(X) is defined as follows. Let X→P (ℕ) denote the set of functions from X to the powerset of the set of natural numbers. Let ≤ denote the binary relation on this set defined by: p ≤ q if and only if there is a partial recursive function φ : ℕ ⇀ ℕ such that for all x ∈ X and n ∈ ℕ, if n ∈ p(x) then φ is defined at n and φ(n) ∈ q(x). Since partial recursive functions are closed under composition and contain the identity function, ≤ is transitive and reflexive, i.e. it is a preorder. Then Prop_{Kℓ}(X) is the quotient of X→P (ℕ) by the equivalence relation generated by ≤; the partial order between equivalence classes [p] is that induced by ≤. Given a function f : Y ⟶ X, the operation f^{∗} : Prop_{Kℓ}(X) ⟶ Prop_{Kℓ}(Y) sends [p] to [p ∘ f]; it is easily seen to be well-defined, monotonic and functorial.

Example 5.2.5 (Subobjects). A important class of examples of propcategories is provided by using the category-theoretic notion of a subobject of an object. Recall that a morphism f : Y ⟶ X in a category C is a monomorphism if for all parallel pairs of morphisms g, h with codomain Y, g = h whenever f ∘ g = f ∘ h. The collection of monomorphisms in C with codomain X can be preordered by declaring that f ≤ f′ if and only if f = f′ ∘ g for some (mono)morphism g. Then a subobject of X is an equivalence class of monomorphisms with codomain X under the equivalence relation generated by ≤. If for each X, there are only a set of such equivalence classes, C is said to be well-powered.

If C has all finite limits and is well-powered, we can make it into a propcategory by taking Prop_{C}(X) to be the set of subobjects of X with partial order that induced by ≤. Given f : Y ⟶ X in C, the operation f^{∗} on subobjects is that induced by pullback along f. (Recall that a pullback of a monomorphism is again a monomorphism.) When C = Set, we obtain an example that is isomorphic to example 5.2.2 above. (Subobjects of X in Set are in natural bijection with subsets of X.) But note that under a similar isomorphism for C = Cpo, the structure in example 5.2.3 picks out a restricted collection subobjects. (Not every subobject of X in Cpo corresponds to an inclusive subset X—consider for example the subobject determined by identity function from the unordered two element set to the ordered two element set.)

Much of the development of the categorical approach to predicate logic (such as the classic text by Makkai and Reyes [1977]) has restricted its attention to interpretations in this class of examples, where formulas (in context) are interpreted as subobjects in categories.

Given a signature Sg of sort, function and relation symbols as in section 5.1, a structure for Sg in a prop-category C is specified by giving an object [[σ]] in C for each sort σ, a morphism [[F]] : [[σ_{1}]] × ⋯ × [[σ_{n}]] ⟶ [[τ]] in C for each function symbol F : σ_{1}, …, σ_{n} ⟶ τ, and a C-property [[R]] ∈ Prop_{C}([[σ_{1}]] × ⋯ × [[σ_{n}]]) for each relation symbol R ⊆ σ_{1}, …, σ_{n}. For each context Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}] and formula ϕ over the signature for which the judgement ϕ prop [Γ] is derivable, we will define a C-property

[[ϕ[Γ]]] ∈ Prop_{C}([[Γ]])

where [[Γ]] denotes the product [[σ_{1}]]×⋯×[[σ_{n}]]. The definition will be given by induction on the derivation of ϕprop [Γ], since there will be at most one way to derive the well-formedness of a formula in a given context. At the moment we only have one rule for forming formulas, namely rule (5.1) for forming atomic formulas. To define [[ϕ[Γ]]] in this case we use the semantics of terms-in-context described in Section 2 to assign meanings [[M_{i}[Γ]]] in the structure for the terms M_{i} and then define

[[R(M_{1}, …, M_{n})[Γ]]] =^{def} ⟨[[M_{1}[Γ]]], … [[M_{n}[Γ]]]⟩^{∗}([[R]]) .

The following lemma is a consequence of Lemma 2.2.1 specifying the behaviour of the categorical semantics with respect to substitution of terms for variables in terms.

Lemma 5.2.6 (Semantics of substitution and weakening). In the categorical semantics of formulas in context, substitution of a term for a variable in a formula is interpreted via the pullback operations. Specifically, if M_{i} : σ_{i} [Γ] for i = 1, …, n, and if ϕ prop [Γ′] with Γ′ = x_{1} : σ_{1}, …, σ_{n}, then

[[(ϕ[M⃗/x⃗])[Γ]]] = ⟨[[M_{1}[Γ]]], …, [[M_{n}[Γ]]]⟩^{∗}([[ϕ[Γ′]]])

where ϕ[M⃗/x⃗] denotes the result of simultaneously substituting M_{i} for x_{i} (i = 1, …, n) in ϕ.

Similarly, weakening of contexts is interpreted via pullback along a product projection: if ϕ prop [Γ], then

[[ϕ[Γ, x : σ]]] = π_{1}^{∗}([[ϕ[Γ]]])

where π_{1}^{∗} : [[Γ, x : σ]] = [[Γ]] × [[σ]] ⟶ [[Γ]] is the product projection in C.

5.3 Satisfaction

Suppose that ϕ_{1}, …, ϕ_{n} ⊢ ψ [Γ] is a sequent over a given signature Sg. Given a structure for Sg in a prop-category C, what should it mean for the structure to satisfy the sequent? Since ϕ_{i} prop [Γ] and ψ prop [Γ] are required to hold, we get C-properties [[ϕ_{i}[Γ]]] and [[ψ[Γ]]] of the object [[Γ]]. In the case n = 1 when the sequent contains a single antecedent formula, it seems natural to define the satisfaction of the sequent to mean that [[ϕ_{i}[Γ]]] ≤ [[ψ[Γ]]] holds in the poset Prop_{C}([[Γ]]). For the general case, let us suppose that each poset Prop_{C}(X) comes equipped with a distinguished element ⊤_{X} and a binary operation A, A′ ↦ A ∧ A′. Then we can define Φ ⊢ ψ [Γ] to be satisfied if

[[Φ[Γ]]] ≤ [[ψ[Γ]]]

where [[Φ[Γ]]] is defined by induction on the length of the list Φ:

[[∅[Γ]]] =^{def} ⊤_{X}
[[Φ, ψ[Γ]]] =^{def} [[Φ[Γ]]] ∧ [[ψ[Γ]]].

We require this definition of satisfaction be sound for the rules in Fig. 2: if the hypotheses of a rule are satisfied so should be the conclusion. For (Cut) to be sound in the case that Φ′ = ∅, it is sufficient that for all A, B, C ∈ Prop_{C}(X), if A ≤ B and ⊤_{X} ∧ B ≤ C then A ≤ C. For (Id) to be sound, it is sufficient that A ∧ B ≤ B. From these two properties plus the fact that ≤ is a partial order, it follows that ⊤_{X} ∧ A = A. Using this, the soundness of (Exchange) amounts to requiring A ∧ B = B ∧ A. But then we have both A ∧ B ≤ B and A ∧ B = B ∧ A ≤ A; so A ∧ B is a lower bound for A and B. In particular for all A, A = ⊤_{X} ∧ A ≤ ⊤_{X}, so that ⊤_{X} is the greatest element of Prop_{C}(X). In fact A ∧ B has to be the greatest lower bound of A and B: for the soundness of (Contract) requires C ≤ C ∧ C, for all C; and the general form of (Cut) (when Φ′ is nonempty) requires for all A, A′, B, C ∈ Prop_{C}(X), if A ≤ B and A′ ∧ B ≤ C then A ∧ A′ ≤ C. The latter property implies that ∧ is monotone, and hence C ≤ A and C ≤ B imply C ≤ C ∧ C ≤ A ∧ B. So all in all, we need each poset Prop_{C}(X) to have finite meets. But that is not all: in view of Lemma 5.2.6, for the soundness of rules (Weaken) and (Subst) we will need that these finite meets be preserved by the pullback operations f^{∗} in C. Therefore we are led to the following definition.

Definition 5.3.1. A prop-category C has finite meets if for each object X in C the poset Prop_{C}(X) possesses all finite meets and these are preserved by the pullback operations f^{∗}. Thus for each X there is ⊤_{X} ∈ Prop_{C}(X) satisfying

• A ≤ ⊤_{X}, for all A ∈ Prop_{C}(X)

• f^{∗}(⊤_{X}) = ⊤_{Y}, for all f : Y ⟶ X;

and for all A, B ∈ Prop_{C}(X), there is an element A ∧ B ∈ Prop_{C}(X) satisfying

• for all C ∈ Prop_{C}(X), C ≤ A ∧ B if and only if C ≤ A and C ≤ B • f^{∗}(A ∧ B) = f^{∗}A ∧ f^{∗}B, for all f : Y ⟶ X.

Given a structure in C for a signature Sg, we say that a sequent Φ ⊢ ψ [Γ] over Sg is satisfied by the structure if

⋀_{ϕ∈Φ}[[ϕ[Γ]]] ≤ [[ψ[Γ]]]  (5.3)

where the left-hand side indicates the (finite) meet of the elements [[ϕ[Γ]]].

Extending Theorem 2.2.3 we have:

Theorem 5.3.2 (Soundness). Let C be a prop-category that has finite meets and let Th be a theory in the sense of Section 5.1. Then any structure in C for the underlying signature of Th that satisfies the axioms of Th also satisfies its theorems.

Examples 5.3.3. The prop-categories of Examples 5.2.2–5.2.5 all have finite meets. Meets in Set (respectively Cpo) are given by set-theoretic intersection of subsets (respectively inclusive subsets)—these are clearly preserved by the pullback operations since these are given by taking inverse images of subsets along functions (respectively ω continuous functions).

Finite meets in Kℓ can be calculated as follows. Choose some recursive bijection pr : ℕ × ℕ ⟶ ℕ and define a binary operation on subsets A, B ⊆ ℕ by

A ∧ B =^{def} {pr(n, m) | n ∈ A and m ∈ B}

Then one can show that for any pair of Kℓ-properties of a set X represented by functions p, q : X ⟶ P (ℕ) say, the meet of [p] and [q] in Prop_{Kℓ}(X) is represented by the function n ↦ p(n) ∧ q(n). The greatest element ⊤_{X} ∈ Prop_{Kℓ}(X) is represented by the function n ↦ ℕ. Since the pullback operations f^{∗} in Kℓ are given by pre-composition with f, it is clear from these descriptions that finite meets are preserved by f^{∗}.

Finally, let C be a category with finite limits, made into a prop-category as in Example 5.2.5 by taking the C-properties of an object X to be its subobjects. Then the top subobject ⊤_{X} is represented by the identity on X; clearly this is stable under pullback. Given two subobjects represented by monomorphisms A ⟶ X, B ⟶ X say, their binary meet is represented by the composition A ∧ B ⟶ A ⟶ X, where A ∧ B ⟶ A is the categorical pullback of B ⟶ X along A ⟶ X. Elementary properties of pullbacks in categories guarantee that this meet operation is stable under pullback.

5.4 Propositional connectives

Given the well-known connection between intuitionistic propositional logic and Heyting algebras (see [Dummett, 1977, Chp. 5], for example), it is not surprising that to model these propositional connectives in a prop-category we will need each poset Prop_{C}(X) to be a Heyting algebra. However, we also require that the Heyting algebra structure be preserved by the pullback operations f^{∗}. This is because these operations will be used in the categorical semantics to interpret the operation of substituting terms for variables in a formula.

Definition 5.4.1. Let C be a prop-category.

(i) C has finite joins if for each object X in C the poset Prop_{C}(X) possesses all finite joins and these are preserved by the pullback operations f^{∗}. Thus for each X there is ⊥_{X} ∈ Prop_{C}(X) satisfying

∗ ⊥_{X} ≤ A, for all A ∈ Prop_{C}(X)

∗ f^{∗}(⊥_{X}) = ⊥_{Y}, for all f : Y ⟶ X; and for all A, B ∈ Prop_{C}(X), there is an element A ∨ B ∈ Prop_{C}(X) satisfying

∗ for all C ∈ Prop_{C}(X), A ∨ B ≤ C if and only if A ≤ C and

B ≤ C

∗ f^{∗}(A ∨ B) = f^{∗}A ∨ f^{∗}B, for all f : Y ⟶ X. (ii) C has Heyting implications (also called ‘relative pseudocomplements’)

if it has finite meets (cf. Definition 5.3.1) and for each object X and all A, B ∈ Prop_{C}(X), there is an element A → B ∈ Prop_{C}(X) satisfying ∗ for all C ∈ Prop_{C}(X), C ≤ A → B if and only if C ∧ A ≤ B ∗ f^{∗}(A → B) = f^{∗}A → f^{∗}B, for all f : Y ⟶ X.

Given a signature Sg as in Section 5.1, consider compound formulas built up from the atomic ones and the propositional constant false using the propositional connectives & (conjunction), ∨ (disjunction), and ⇒ (implication). The rules of formation are

false prop [Γ]  (5.4)

ϕ prop [Γ] ϕ′ prop [Γ]

(where # is one of &, ∨, ⇒)

ϕ#ϕ′ prop [Γ]

(5.5)

Negation, ¬ϕ, will be treated as an abbreviation of ϕ ⇒ false; truth, true, will be treated as an abbreviation of ¬false; bi-implication, ϕ ⇔ ϕ′, will be treated as an abbreviation of (ϕ ⇒ ϕ′) &(ϕ′ ⇒ ϕ).

Given a structure for Sg in a prop-category C with finite meets, finite joins and Heyting implications, we can interpret formulas-in-context ϕ[Γ] as C-properties [[ϕ[Γ]]] ∈ Prop_{C}([[Γ]]), by induction on the derivation of ϕ prop [Γ]. Atomic formulas are interpreted as in Section 5.3, and compound formulas as follows:

[[false[Γ]]] =^{def} ⊥_{[[Γ]]}
[[ϕ & ϕ′[Γ]]] =^{def} [[ϕ[Γ]]] ∧ [[ϕ′[Γ]]]
[[ϕ ∨ ϕ′[Γ]]] =^{def} [[ϕ[Γ]]] ∨ [[ϕ′[Γ]]]
[[ϕ ⇒ ϕ′[Γ]]] =^{def} [[ϕ[Γ]]] →[[ϕ′[Γ]]]

In this way the notion given in Section 5.3 of satisfaction of a sequent by a structure applies to sequents involving the propositional connectives.

Theorem 5.4.2 (Soundness). Given a structure in a prop-category C with finite meets, finite joins and Heyting implications, the collection of sequents Φ ⊢ ψ [Γ] that are satisfied by the structure (cf. 5.3) is closed under the usual introduction and elimination introduction rules for the propositional connectives in Gentzen’s Natural Deduction formulation of the intuitionistic sequent calculus, set out in Fig. 3.

Recall that a poset P can be regarded as a category whose objects are the elements of P and whose morphisms are instances of the order relation. From this point of view, meets, joins, and Heyting implications are all instances of adjoint functors. The operation of taking the meet (respectively the join) of n elements is right (respectively left) adjoint to the diagonal functor P ⟶ P^{n}; and given A ∈ P, the Heyting implication operation A →(−) : P ⟶ P is right adjoint to (−) ∧ A : P ⟶ P. Fig. 4 gives an alternative formulation of the rules for the intuitionistic propositional connectives reflecting this adjoint formulation. The rules take the form

Φ ⊢ false

(false-Elim) Φ ⊢ ψ

Φ ⊢ ψ Φ′ ⊢ ψ′

(&-Intr)

Φ, Φ′ ⊢ ψ & ψ′

Φ ⊢ ψ & ψ′ ; (&-Elim_{1}) ; Φ ⊢ ψ Φ ⊢ ψ & ψ′ ; (&-Elim_{2}) ; Φ ⊢ ψ′

Φ ⊢ ψ ; (∨-Intr_{1}) ; Φ ⊢ ψ ∨ ψ′  Φ ⊢ ψ′ ; (∨-Intr_{2}) ; Φ ⊢ ψ ∨ ψ′

Φ, ψ ⊢ θ Φ′, ψ′ ⊢ θ Φ′′ ⊢ ψ ∨ ψ′

(∨-Elim)

Φ, Φ′, Φ′′ ⊢ θ

Φ, ψ ⊢ ψ′ ; (⇒-Intr) ; Φ ⊢ ψ ⇒ ψ′ Φ ⊢ ψ ⇒ ψ′ Φ′ ⊢ ψ

(⇒-Elim)
Φ, Φ′ ⊢ ψ

Fig. 3. Natural Deduction rules for intuitionistic propositional connectives

Φ ⊢ ψ Φ ⊢ ψ′ ; = (&-Adj ) ; Φ ⊢ ψ & ψ′  Φ, ψ ⊢ θ Φ, ψ′ ⊢ θ ; = (∨-Adj ) ; Φ, ψ ∨ ψ′ ⊢ θ

Φ, ψ ⊢ ψ′ ; = (⇒-Adj ) ; Φ ⊢ ψ ⇒ ψ′

= (false-Adj ) Φ, false ⊢ ψ

Fig. 4. ‘Adjoint’ rules for intuitionistic propositional connectives

sequents = sequent

A set of sequents is closed under such a ‘bi-rule’ if the set contains the sequents above the double line if and only if it contains the sequent below the double line; such a rule is thus an abbreviation for several ‘uni-directional’ rules.

Note that the presence of the extra formulas Φ in rule (∨-Adj ) means that the character of disjunction is captured not just by the left adjointness property of binary joins—one also needs the adjoint to possess a ‘stability’ property which in this case is the distribution of finite meets over finite joins. (Compare this with the need identified in Section 3.1 for coproducts to be stable in order to model disjoint union types correctly.) In the presence of rule (⇒-Adj ) this stability property is automatic, and we could have given the rule without the extra formulas Φ. ((false-Adj ) is also a ‘stable’ left adjunction rule, but in this case the stability gives rise to no extra condition.)

The proof of the Soundness Theorem 5.4.2 amounts to showing that the rules in Fig. 3 are derived rules of Fig. 4. Conversely, it is not hard to prove that the (uni-directional versions of) the rules in Fig. 4 are derived rules of Fig. 3. In this sense, the two presentations give equivalent formulations of provability (i.e. what can be proved in intuitionistic propositional logic. However, the structure of proofs in the two formulations may be very different. One should note that the presence of rule (Cut) (which corresponds to the transitivity of ≤ in prop-categories) in Fig. 4 is apparently essential for the adjoint formulation to be equivalent to the natural deduction formulation of Fig. 3—unlike the situation for Gentzen’s Sequent Calculus formulation where cuts can be eliminated (see [Dummett, 1977, 4.3]).

Remark 5.4.3. A typical feature of the categorical treatment of logical constructs is the identification of which constructs are essentially uniquely determined by their logical properties. Adjoint functors are unique up to isomorphism if they exist. So in particular the operations of Definitions 5.3.1 and 5.4.1 are uniquely determined if they exist for C. Correspondingly, the adjoint rules of Fig. 4 make plain that up to provable equivalence, the intuitionistic connectives are uniquely determined by their logical properties. For example, there cannot be two different binary meet operations on a poset, and correspondingly if &′ were another connective satisfying rule (& − Adj ), then ∅ ⊢ (ϕ & ϕ′) ⇔(ϕ &′ ϕ′) would be provable for all ϕ, ϕ′. Such uniqueness for logical constructs does not always hold: for example the exponential operator (!) of Girard’s Linear Logic [1987] does not have this property.

Example 5.4.4. The prop-category Set of Example 5.2.2 has finite meets and finite joins, given by set-theoretic intersection and union respectively (which are preserved by the pullback operations since these are given by taking inverse images along functions). Indeed, each Prop_{Set}(X) is a Boolean algebra and so the categorical semantics of formulas is sound for classical propositional logic. This semantics coincides with the usual set-theoretic one, in the sense that the subset [[ϕ[x_{1} : σ_{1}, …, x_{n} : σ_{n}]]] ⊆ [[σ_{1}]] × ⋯ × [[σ_{n}]] consists of those n-tuples (a_{1}, …, a_{n}) for which the sentence ϕ[a_{1}/x_{1}, …, a_{n}/x_{n}] is satisfied in the classical, Tarskian sense (see [Chang and Keisler, 1973, 1.3]).

Example 5.4.5. Turning to the prop-category Cpo of Example 5.2.3, first note that each poset Prop_{Cpo}(X) does have meets, joins and Heyting implications. Meets (even infinite ones) are given by set-theoretic intersection. Finite joins are given by set-theoretic union. The Heyting implication A → B of inclusive subsets A, B ∈ Prop_{Cpo}(X) is given by taking the intersection of all inclusive subsets of X that contain A \ B = {x ∈ X | x ∉ A or x ∈ B}.

The operation f^{∗} of taking the inverse image of an inclusive subset along an ω-continuous function f : Y ⟶ X preserves meets and finite joins, but it does not preserve Heyting implications. (For example, take X to be the successor ordinal ω^{+}, Y to be the discrete ω-cpo with the same set of elements, and f to be the identity function; when A = {ω} and B = ∅, one has f^{∗}(A → B) = f^{∗}(X) = Y ≠ ω = f^{∗}A → f^{∗}B.) Thus Cpo supports the interpretation of conjunction and disjunction, but not implication.

Example 5.4.6. The prop-category Kℓ of Example 5.2.4 has finite meets, finite joins and Heyting implications. To see this one needs to consider numerical codes for partial recursive functions. Let n · x denote the result, if defined, of applying the nth partial recursive function (in some standard enumeration) to x. The notation {n}(x) is traditional for n · x. We will often write nx for n·x; a multiple application (n·x)·y will be written nxy, using the convention that − · − associates to the left.

So for each partial recursive function φ : ℕ ⇀ ℕ there is some n ∈ ℕ such that nx ≍ φ(x) for all x ∈ ℕ. Here ‘e ≍ e’ means ‘e⇓ if and only if e′⇓, in which case e = e′’, and ‘e⇓’ means ‘the expression e is defined’. The key requirement of this enumeration of partial recursive functions is that the partial binary operation n, m ↦ n · m makes ℕ into a ‘partial combinatory algebra’—i.e. there should be K, S ∈ ℕ satisfying for all x, y, z ∈ ℕ that

Kx⇓ and Kx ≍ x
Sx⇓, Sxy⇓ and Sxyz ≍ xz(yz)

In particular K and S can be used to define P, P_{0}, P_{1} ∈ ℕ so that (x, y) ↦ Pxy defines a recursive bijection ℕ × ℕ ≅ ℕ with inverse z ↦ (P_{0}z, P_{1}z).

Now define three binary operations on subsets A, B ⊆ ℕ as follows:

A ∧ B =^{def} {Pxy | x ∈ A and y ∈ B}
A ∨ B =^{def} {P_{0}x | x ∈ A} ∪ {P_{1}y | y ∈ A}
A → B =^{def} {n | for all x ∈ A, nx⇓ and nx ∈ B}

Using elementary properties of the partial combinatory algebra (ℕ, ·) one can show that for any pair of Kℓ-properties of a set X, represented by functions p, q : X ⟶ P (ℕ) say, the meet of [p] and [q] in Prop_{Kℓ}(X) is represented by the function n ↦ p(n) ∧ q(n). Similarly their join is represented by the function n ↦ p(n) ∨ q(n) and their Heyting implication is represented by the function n ↦ p(n) → q(n). The greatest and least elements ⊤_{X}, ⊥_{X} ∈ Prop_{Kℓ}(X) are represented by the functions n ↦ ℕ and n ↦ ∅ respectively. Since the pullback operations f^{∗} in Kℓ are given by pre-composition with f, it is clear from these descriptions that finite meets, finite joins and Heyting implications are all preserved by f^{∗}.

So the prop-category Kℓ supports an interpretation of the propositional connectives that is sound for intuitionistic logic. Combining the definition of the categorical semantics with the above description of finite meets, finite joins and Heyting implications in Kℓ one finds that this interpretation is in fact Kleene’s ‘1945-realizability’ explanation of the intuitionistic propositional connectives (see [Dummett, 1977, 6.2]), in the sense that the relation ‘n ∈ [[ϕ[ ]]]’ coincides with the relation ‘n realizes ϕ’.

Remark 5.4.7 (Classical logic). We can obtain classical propositional logic by adding the rule

{Φ ⊢ ¬¬ψ \atop Φ ⊢ ψ}

to those in Fig. 3. Recalling that ¬ψ is an abbreviation for ψ ⇒ false, one has that [[¬ψ[Γ]]] is the pseudocomplement of [[ψ[Γ]]] in the Heyting algebra Prop_{C}([[Γ]]). For the above rule to be sound in C we need ((A → ⊥_{X}) → ⊥_{X}) ≤ A to hold for each A ∈ Prop_{C}(X). In other words the pseudocomplement of every C-property must actually be a complement. So to obtain a sound (and in fact complete) semantics for classical propositional logic we require that each Prop_{C}(X) is a Boolean algebra and that each pullback operation f^{∗} preserve finite meets and joins (and hence also complements).

5.5 Quantification

The rules for forming quantified formulas are

ϕ(x) prop [x : σ] ∀_{σ}(ϕ) prop  ϕ(x) prop [x : σ] ∃_{σ}(ϕ) prop .

The usual Natural Deduction rules for introducing and eliminating quantifiers are given in Fig. 5. Modulo the structural rules of Fig. 2, these Natural Deduction rules are inter-derivable with an ‘adjoint’ formulation given by the bi-directional rules of Fig. 6. It should be noted that some side conditions are implicit in these rules because of the well-formedness conditions mentioned after (5.2) that are part of the definition of a sequent. Thus x does not occur free in Φ in (∀-Intro) or (∀-Adj ); and it does not occur free in Φ, Φ′, θ in (∃-Elim) or (∃-Adj ).

What structure in a prop-category C with finite meets is needed to soundly interpret quantifiers? Clearly we need functions

Φ ⊢ ψ(x) [x : σ] ; (∀-Intr) ; Φ ⊢ ∀_{σ}(ψ)  Φ ⊢ ∀_{σ}(ψ) M : σ ; (∀-Elim) ; Φ ⊢ ψ(M)

Φ ⊢ ψ(M) ; (∃-Intr) ; Φ ⊢ ∃_{σ}(ψ) Φ ⊢ ∃_{σ}(ψ) Φ′, ψ(x) ⊢ θ [x : σ]

(∃-Elim)
Φ, Φ′ ⊢ θ

Fig. 5. Natural Deduction rules for quantifiers

Φ ⊢ ψ(x) [x : σ]
= (∀-Adj )
Φ ⊢ ∀_{σ}(ψ)

Φ, ψ(x) ⊢ θ [x : σ]
= (∃-Adj)
Φ, ∃_{σ}(ψ) ⊢ θ

Fig. 6. ‘Adjoint’ rules for quantifiers

⋀I,X , _{⋁I,X} : Prop_{C}(I × X) ⟶ Prop_{C}(I)

so that we can define

[[∀_{σ}(ϕ)[Γ]]] =^{def} _{⋀[[Γ]],[[σ]]}([[ϕ(x)[Γ, x : σ]]])
[[∃_{σ}(ϕ)[Γ]]] =^{def} _{⋁[[Γ]],[[σ]]}([[ϕ(x)[Γ, x : σ]]]) .

In order to retain the soundness of the structural rules (Weaken) and (Subst), we must require that these operations be natural in I, i.e. for any f : I′ ⟶ I we require

f^{∗}(_{⋀I,X}A) = _{⋀I_{′},X}((f × id_{X})^{∗}A)  (5.6)
f^{∗}(_{⋁I,X}A) = _{⋁I_{′},X}((f × id_{X})^{∗}A) .  (5.7)

Given the semantics of weakening in Lemma 5.2.6, for the soundness of (∀-Adj ) we need

A ≤ _{⋀I,X}(B) ⇔ π_{1}^{∗}(A) ≤ B  (5.8)

for all A ∈ Prop_{C}(I) and B ∈ Prop_{C}(I × X). In other words _{⋀I,X} provides a right adjoint to the monotone function

π_{1}^{∗} : Prop_{C}(I) ⟶ Prop_{C}(I × X) .

Note that this requirement determines the function _{⋀I,X} uniquely and implies in particular that it is a monotone function.

Given the definition of satisfaction of sequents in Section 5.3, for the soundness of (∃-Adj ) we need

A ∧_{⋁I,X}(B) ≤ C ⇔ π_{1}^{∗}(A) ∧ B ≤ π_{1}^{∗}(C)

for all A, C ∈ Prop_{C}(I) and B ∈ Prop_{C}(I × X). We can split this requirement into two: first that _{⋁I,X} provides a left adjoint to π_{1}^{∗}, and secondly a ‘stability’ condition for the left adjoint with respect to meets:

⋁I,X(B) ≤ C ⇔ B ≤ π_{1}^{∗}(C)  (5.9)
A ∧_{⋁I,X}(B) = _{⋁I,X}(π_{1}^{∗}(A) ∧ B) .  (5.10)

Definition 5.5.1. Let C be a prop-category with finite meets. We say that C has universal quantification if for each product projection π_{1} : I × X ⟶ X in C, the pullback function π_{1}^{∗} possesses a right adjoint _{⋀I,X} (5.6) and these right adjoints are natural in I (5.6).

We say that C has existential quantification if each π_{1}^{∗} possesses a left adjoint _{⋁I,X} (5.9) and these left adjoints are both natural in I (5.7) and satisfy the stability condition (5.10).

Thus we have shown that if C is a prop-category with finite meets and both universal and existential quantification, then the sequents that are satisfied by a structure in C are closed under the quantifier rules in Fig. 5.

Remark 5.5.2. Conditions (5.6) and (5.7) are instances of what Lawvere [1969] termed the ‘Beck-Chevalley Condition’: see Remark 5.6.6. Condition (5.10) was called by him ‘Frobenius Reciprocity’. It is somewhat analogous to the stability condition on coproducts needed in Section 3.1 to soundly interpret disjoint union types. Just as there we noted that the existence of exponentials makes stability of coproducts automatic, so here it is the case that condition (5.10) holds automatically if C has Heyting implications (see Definition 5.4.1).

Example 5.5.3. The prop-cat Set of Example 5.2.2 possesses adjoints for all pullback operations and in particular for pullback along projections. Specifically, for A ⊆ I × X we have

⋀I,X(A) = {i ∈ I | ∀x ∈ X.(i, x) ∈ A}
⋁I,X(A) = {i ∈ I | ∃x ∈ X.(i, x) ∈ A} .

These adjoints are easily seen to be natural in I, and since Set has Heyting (indeed Boolean) implications, as noted above the Frobenius Reciprocity condition (5.10) holds automatically.

Thus Set has both universal and existential quantification. Given the above formulas for the adjoints, it is clear that the remark in Example 5.4.4 about the coincidence categorical semantics in Set with the usual, Tarskian semantics of formulas continues to hold in the presence of quantified formulas.

Example 5.5.4. The prop-category Kℓ of Example 5.2.2 also has universal and existential quantification. Given A ∈ Prop_{Kℓ}(I × X), suppose A is represented by the function p : I × X ⟶ P (ℕ). Then _{⋀I,X}(A) and ⋁I,X(A) can be represented respectively by the functions

α_{I,X}(p) , ϵ_{I,X}(p) : I ⟶ P (ℕ)

defined by

α_{I,X}(p)(i) = ⋂_{x∈X} p(i, x) and ϵ_{I,X}(p)(i) = ⋃_{x∈X} p(i, x) .

Some calculations with partial recursive functions show that these formulas do indeed yield the required adjoints, and that they are natural in I. Since we noted in Example 5.4.6 that Kℓ has Heyting implications, the Frobenius Reciprocity condition (5.10) holds automatically.

Example 5.5.5. The prop-category Cpo of Example 5.2.3 possesses natural right adjoints to pulling back along projections: they are given just as for Set by the formula (5.11), since this is an inclusive subset when A is. Cpo also possesses left adjoint to pulling back along projections: ⋁I,X(A) is given by the smallest inclusive subset of I containing {i ∈ I | ∃x ∈ X.(i, x) ∈ A} (i.e. by the intersection of all inclusive subsets containing that set). However, these left adjoints do not satisfy the Beck-Chevalley condition (5.7). For if this condition did hold, for any i ∈ I we could apply it with I′ a one-element ω-cpo and f : I′ ⟶ I the function mapping the unique element of I′ to i, to conclude that i ∈ _{⋁I,X}(A) if and only if (i, x) ∈ A for some x ∈ X. In other words the set in (5.11) would already be inclusive when A is inclusive. But this is by no means the case in general. (For example consider when I is the successor ordinal ω^{+} and X is the discrete ω-cpo with the same set of elements. Then A = {(m, n) | m ≤ n} is an inclusive subset of I × X, but (5.11) is ω, which is not an inclusive subset of ω^{+}.)

Thus the prop-category Cpo has universal quantification, but not existential quantification.

5.6 Equality

We have seen that the categorical semantics of the propositional connectives and quantifiers provides a characterization of these logical operations in terms of various categorical adjunctions. In this section we show that, M : σ

(=-Intr)

Φ ⊢ (M =_{σ} M)

Φ ⊢ (M =_{σ} M′) Φ′ ⊢ ψ(x, x) [x : σ]

(=-Elim)

Φ, Φ′ ⊢ ψ(M, M′)

Fig. 7. Natural Deduction rules for equality

Φ ⊢ ψ(x, x) [x : σ]

= (=-Adj )

Φ, (x =_{σ} x′) ⊢ ψ(x, x′) [x : σ, x′ : σ]

Fig. 8. ‘Adjoint’ rule for equality

within the context of first-order logic, the same is true of equality predicates. (As with so much of categorical logic, this observation originated with Lawvere [1970].) The formation rule for equality formulas is

M : σ M′ : σ
.
(M =_{σ} M′) prop

Natural Deduction rules for introducing and eliminating such formulas are given in Fig. 7 (cf. [Nordström et al., 1990, Section 8.1]). The usual properties of equality, such as reflexivity, symmetry, and transitivity, can be derived from these rules. It is not hard to see that modulo the structural rules of Fig. 2, the Natural Deduction rules are inter-derivable with an ‘adjoint’ formulation given by the bi-directional rule of Fig. 8.

Suppose C is a prop-category with finite meets. To interpret equality formulas whilst respecting the structural rules (Weaken) and (Subst) of Fig. 2, for each C-object X we need a C-property

Eq_{X} ∈ Prop_{C}(X × X)

so that we can define

[[(M =_{σ} M′)[Γ]]] =^{def} ⟨[[M[Γ]]], [[M′[Γ]]]⟩^{∗}(Eq_{[[σ]]}) .  (5.11)

Given the definition of satisfaction of sequents in Section 5.3, for the soundness of (=-Adj ) we need

A ≤ (id_{I} × Δ_{X})^{∗}(B) ⇔ (id_{I} × π_{1})^{∗}(A) ∧ π_{2}^{∗}(Eq_{X}) ≤ B (5.12)

for all C-objects I, X and all C-properties A ∈ Prop_{C}(I × X) and B ∈ Prop_{C}(I × (X × X)). Here Δ_{X} is the diagonal morphism ⟨id_{X}, id_{X}⟩ : X ⟶ X × X, and π_{1} and π_{2} are the product projections X × X ⟶ X and I × (X × X) ⟶ X × X.

Condition (5.12) says that for each A ∈ Prop_{C}(I × X), the value of the left adjoint to (id_{I} × Δ_{X})^{∗} exists at A and is equal to (id_{I} × π_{1})^{∗}(A) ∧ π_{2}^{∗}(Eq_{X}). In particular, taking I to be the terminal object in C and A = ⊤_{I×X}, we have that Eq_{X} is the value of the left adjoint to Δ_{X}^{∗} at the top element ⊤_{X} ∈ Prop_{C}(X), i.e.

⊤_{X} ≤ Δ_{X}^{∗}(B) ⇔ Eq_{X} ≤ B  (5.13)

for all B ∈ Prop_{C}(X × X). Note that the C-properties Eq_{X} are uniquely determined by this requirement.

Definition 5.6.1. Let C be a prop-category with finite meets. We say that C has equality if for each C object X, the value Eq_{X} of the left adjoint to Δ_{X}^{∗} at the top element ⊤_{X} ∈ Prop_{C}(X) exists and satisfies (5.12)

Thus we have shown that if C is a prop-category with finite meets and equality, then the sequents that are satisfied by a structure in C are closed under the equality rules in Fig. 7.

Remark 5.6.2. In fact when C also has Heyting implications and universal quantification, then property (5.12) is automatic if Eq_{X} exists satisfying (5.13). This observation corresponds to the fact that in the presence of implication and universal quantification, the rule (=-Adj ) is inter-derivable with a simpler rule without ‘parameters’:

∅ ⊢ ψ(x, x) [x : σ]
.
(x =_{σ} x′) ⊢ ψ(x, x′) [x : σ, x′ : σ]

Example 5.6.3. The prop-category Set of Example 5.2.2 has equality. Since we have seen in previous sections that Set has implication and universal quantification, by Remark 5.6.2 it suffices to establish the existence of the left adjoint to Δ_{X}^{∗} at ⊤_{X}. But for this, clearly we can take Eq_{X} ⊆ X×X to be the identity relation {(x, x) | x ∈ X}.

Similarly for the prop-category Kℓ of Example 5.2.4, since it has implication and universal quantification, to see that it also has equality we just have to verify (5.13). This can be done by taking taking Eq_{X} to be the Kℓ-property represented by the function δ_{X} : X × X ⟶ P (ℕ) defined by

δ_{X}(x, x′) =^{def} \{ \begin{matrix}ℕ & if x = x′ \\ ∅ & if x ≠ x′ . \end{matrix}

Example 5.6.4. We saw in Example 5.4.5 that prop-category Cpo does not have Heyting implications. Hence condition (5.12) is not necessarily implied by the special case (5.13) in this case. Nevertheless, we can satisfy (5.12) by taking each Eq_{X} to be the inclusive subset {(x, x) | x ∈ X} of the ω-cpo X × X. Thus Cpo does have equality.

Example 5.6.5. Let C be a category with finite limits, made into a propcategory (with finite meets) as in Example 5.2.5. Then C has equality, with Eq_{X} the subobject of X × X represented by the diagonal monomorphism Δ_{X} = ⟨id_{X}, id_{X}⟩. Note that in this case, definition (5.11) implies that the interpretation [[(M =_{σ} M′)[Γ]]] of an equality formula is the subobject of [[Γ]] represented by the equalizer of the pair of C-morphisms

[[M[Γ]]] , [[M′[Γ]]] : [[Γ]] ⟶ [[σ]] .

Remark 5.6.6 (Generalized quantifiers). Suppose that C is a propcategory with finite meets, Heyting implications and both universal and existential quantification. Then not only do the adjoints _{⋀I,X},_{⋁I,X} exist, but in fact for any C morphism f : X ⟶ Y, the monotone function f^{∗} : Prop_{C}(Y) ⟶ Prop_{C}(X) has both left and right adjoints, which will be denoted _{⋁f} and _{⋀f} respectively. Indeed, for B ∈ Prop_{C}(Y) we can define

⋁f(A) = _{⋁X,Y} ((f × id_{Y})^{∗}(Eq_{Y}) ∧ π_{1}^{∗}(A))
⋀f(A) = _{⋀X,Y} ((f × id_{Y})^{∗}(Eq_{Y}) → π_{1}^{∗}(A)) .

It is easier to see what these expressions mean and to prove that they have the required adjointness properties if we work in a suitable internal language for the prop-category C. The signature of such an internal language is like that discussed in Section 2.3, but augmented with relation symbols R ⊆ X_{1} × ⋯ × X_{n} for each C-property R ∈ Prop_{C}(X_{1} × ⋯ × X_{n}) (for each tuple of C-objects X_{1}, …, X_{n}). Using the obvious structure in C for this signature, one can describe C-properties using the interpretation of formulas over the signature; and relations between such C-properties can be established by proving sequents in the predicate calculus and then appealing to the soundness results we have established.

From this perspective _{⋁f} and _{⋀f} are the interpretation of formulas that are generalized quantifiers, adjoint to substitution:

⋁f(A) = [[∃_{σ}(x)(f(x) =_{Y} y & A(x))]]
⋀f(A) = [[∀_{σ}(x)(f(x) =_{Y} y ⇒ A(x))]] .

The adjointness properties

⋁f(A) ≤ B ⇔ A ≤ f^{∗}(B)

B ≤ _{⋀f}(A) ⇔ f^{∗}(B) ≤ A

can be deduced from the fact that the following bi-directional rules are derivable from the Natural Deduction rules for &, ⇒, ∃, ∀, = :

∃_{σ}(x)(f(x) =_{Y} y & A(x)) ⊢ B(y) [y : Y] = A(x) ⊢ B(f(x)) [x : X]

B(y) ⊢ ∀_{σ}(x)(f(x) =_{Y} y ⇒ A(x)) [y : Y] = .

B(f(x)) ⊢ A(x) [x : X]

We required the adjoints_{⋁I,X}( = _{⋁π_{1}}) and_{⋀I,X}( = _{⋀π_{1}}) to be natural in I in order to model the interaction between quantification and substitution correctly. More generally, the adjoints _{⋁f} and _{⋀f} enjoy stability properties reflecting the interaction of the generalized quantifiers with substitution on their parameters. These stability conditions are all instances of what Lawvere [1969] termed Beck-Chevalley conditions. In general if

[figure: X; h; W; Y; f; g; Z; k]

is a commutative square in C, then we say that the left adjoints to the pullback functions satisfy a Beck-Chevalley Condition for the above square if g^{∗}_{⋁k} = _{⋁f}h^{∗}. Note that h^{∗}k^{∗} = f^{∗}g^{∗} (since kh = gf), id_{W} ≤ k^{∗}_{⋁k} (since _{⋁k} is left adjoint to k^{∗}), and _{⋁f}f^{∗} ≤ id_{Y} (since _{⋁f} is left adjoint to f^{∗}); so

⋁fh^{∗} ≤ _{⋁f}h^{∗}k^{∗}_{⋁k} = _{⋁f}f^{∗}g^{∗}_{⋁k} ≤ g^{∗}_{⋁k} .

So the Beck-Chevalley Condition amounts to requiring the other inequality: g^{∗}_{⋁k} ≤ _{⋁f}h^{∗}. Dually, g^{∗}_{⋀k} ≤ _{⋀f}h^{∗} holds automatically and the right adjoints are said to satisfy a Beck-Chevalley condition for the above square if the reverse inequality holds, so that g^{∗}_{⋀k} = _{⋀f}h^{∗}. With this terminology, it is the case that in a prop-category with finite meets, Heyting implications and quantification, the left and right adjoints to the pullback operations satisfy the Beck-Chevalley Condition for certain commutative squares which (by virtue of the finite products in C) are pullback squares. These are the squares of the form

[figure: I × X; π_{1}; X; I × Y; id_{I} × f; π_{1}; Y; f; X; ⟨id_{X}, f⟩; X × Y; Y; f; Δ_{Y}; Y × Y .; f × id_{Y}]

If the underlying category of C has all pullbacks, obviously a sufficient condition to ensure the adjoints to the pullback functions satisfy these stability conditions is that the Beck-Chevalley Condition holds for all pullback squares. (And in fact this holds for the left adjoints if and only if it holds for the right adjoints.) This is the case for the prop-categories Set and Kℓ of Examples 5.2.2 and 5.2.4.

Remark 5.6.7. The version of predicate logic we have described here is somewhat unusual in that it has both equality judgements (M = M′ : σ [Γ]) and equality formulas (M =_{σ} M′), the latter occurring as a constituent of sequent judgments (Φ ⊢ ψ [Γ]). Using the rule (Subst) from Fig. 2 and the rule (=-Intro) from Fig. 7, one can derive the following rule connecting the two forms of equality:

M = M′ : σ
.
∅ ⊢ (M =_{σ} M′)

However, for the converse of this rule to be satisfied in a prop-category with equality it would have to be the case that for any parallel pair of C-morphisms f, f′ : I ⟶ X, that if ⊤_{I} = ⟨f, f′⟩^{∗}(Eq_{X}) then f = f′. This condition holds for the examples given in this section, but not in general. (For example, consider a ‘degenerate’ prop-category whose underlying category is the category of sets and functions and whose poset of properties at each set is the trivial, one-element poset.)

5.7 Completeness

Let Th be a theory whose sequent axioms may involve the propositional connectives, quantifiers and equality. The theorems of such a theory are those judgements that can be derived from the axioms using the rules in Figs 2, 3, 5, and 7, together with the rules for equational logic given in Section 2.1.

Given a prop-category C possessing finite meets, finite joins, Heyting implications, quantification, and equality, a categorical model for Th in C consists of a structure for the signature of the theory with the property that each of the theory’s axioms are satisfied by the structure. The soundness of the categorical semantics implies that every theorem of the theory is also satisfied by such a model. Conversely, the categorical semantics is complete, in the sense that a judgement over the signature of a given theory is a theorem if it is satisfied by all models of the theory in prop-categories with finite meets, finite joins, Heyting implications, quantification, and equality.

This completeness is an easy corollary of the stronger result that, given Th, there is a ‘classifying’ prop-category Cℓ(Th) containing a ‘generic’ model G, which is in particular a structure that satisfies a sequent (or an equation) if and only if it is a theorem of Th. This classifying prop-category can be constructed via an extension of the ‘term-model’ construction discussed in Section 4. The underlying category of the prop-category Cℓ(Th) is constructed just as in Section 4.2: its objects are α-equivalence classes of contexts Γ, and its morphisms are equivalence classes of context morphisms under provable equality in Th.

Then for each object Γ we defined the poset of Cℓ(Th)-properties of Γ as follows. Its underlying set is the quotient

Prop_{Cℓ(Th)}(Γ) =^{def} {ϕ | ϕ prop [Γ]}/ ∼_{Th}

where the equivalence relation ϕ ∼_{Th} ϕ′ holds if and only if both ϕ ⊢ ϕ′ [Γ] and ϕ′ ⊢ ϕ [Γ] are theorems of Th. The partial order on Prop_{Cℓ(Th)}(Γ) is that induced by Th-provable entailment: A ≤ A′ holds if and only if for some (indeed, any) formulas ϕ and ϕ′ representing the equivalence classes A and A′ respectively, ϕ ⊢ ϕ′ [Γ] is a theorem of Th.

To complete the definition of the prop-category structure (cf. Definition 5.2.1), we have to define the action of pulling back a Cℓ(Th)-property along a morphism. This is induced by the operation of substituting terms for variables in formulas. Given A ∈ Prop_{Cℓ(Th)}(Γ) and γ : Γ′ ⟶ Γ with

A = [ϕ]
Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}]
γ = [M_{1}, …, M_{n}]

then

γ^{∗}A =^{def} [ϕ[M_{1}/x_{1}, …, M_{n}/x_{n}]] .

The properties of monotonicity and functoriality of (−)^{∗} in Definition 5.2.1 are easily verified (using the definition of identities and composition in Cℓ(Th) given in Section 4.2.)

Proposition 5.7.1. The classifying prop-category Cℓ(Th) has finite meets, finite joins, Heyting implication, universal and existential quantification, and equality.

Proof. The propositional operations are induced by the corresponding logical connectives. Thus for any object Γ and Cℓ(Th)-properties A = [ϕ] and A′ = [ϕ′] of Γ, we have:

A ∧ A′ = [ϕ & ϕ′]
A ∨ A′ = [ϕ ∨ ϕ′]
A → A′ = [ϕ ⇒ ϕ′]
⊤_{Γ} = [true]
⊥_{Γ} = [false] .

Similarly, quantification is induced by the corresponding operation on formulas. Thus if A = [ϕ] ∈ Prop_{Cℓ(Th)}(Δ × Γ), so that ϕ prop [Δ, Γ], then

⋀Δ,Γ(A) = [∀_{σ_{1}}(x_{1}) ⋯ ∀_{σ_{n}}(x_{n})ϕ]

if Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}] say.

Finally, for each object Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}], the equality property Eq_{Γ} ∈ Prop(Γ × Γ′) can be represented by the formula

(x_{1} =_{σ_{1}} x′_{1}) & ⋯ &(x_{n} =_{σ_{n}} x′_{n})

where the variables x′_{1}, …, x′_{n} are chosen to be distinct from x_{1}, …, x_{n} (and each other).

Turning now to the generic model G of Th in Cℓ(Th), its underlying structure is defined for the types and function symbols of Th as in Section 4.2, and for relation symbols R ⊆ σ_{1}, …, σ_{n} by

G[[R]] =^{def} [R(x_{1}, …, x_{n})] ∈ Prop_{Cℓ(Th)}([x_{1} : σ_{1}, …, x_{n} : σ_{n}]) .

Extending the properties of G on types, terms and equations given in Lemma 4.2.4, we also have the following properties for formulas and sequents.

Lemma 5.7.2. The structure G has the following properties.

(i) If ϕ prop [Γ], then the interpretation G[[ϕ[Γ]]] ∈ Prop_{Cℓ(Th)}(Γ) of the formula ϕ in the structure G is just the Cℓ(Th)-property represented by the formula ϕ.

(ii) Φ ⊢ ψ [Γ] is a theorem of Th if and only if

⋀ϕ∈ΦG[[ϕ[Γ]]] ≤ G[[ψ[Γ]]] .

In other words, G satisfies a sequent just in case it is a theorem of Th. In particular G satisfies the axioms of Th and hence is a model of Th.

Corollary 5.7.3 (Completeness). A judgement over the signature of a given theory is a theorem if it is satisfied by all models of the theory in prop-categories with finite meets, finite joins, Heyting implications, quantification, and equality.

Stronger forms of completeness hold with models of Th restricted to particular classes of prop-category. For example, Kripke’s completeness theorem for intuitionistic predicate logic (see [Dummett, 1977, Chp. 5]) can be paraphrased in category-theoretic terms as asserting the completeness of the collection of prop-categories of the kind given in Example 5.2.5, but with the category C restricted to be a category of set-valued presheaves on a poset.

Remark 5.7.4. The classifying prop-category Cℓ(Th) and the generic algebra G of a predicate theory have a universal property analogous to that given for algebraic theories in Theorem 4.2.5 (but with respect to a suitable notion of morphism of prop-categories). This universal property forms the basis of an equivalence between theories in predicate logic (and translations between them) and suitably structured prop-categories (and morphisms between them)—cf. Section 4.3.

6 Dependent Types

This section considers the categorical semantics of type theories involving types that depend upon terms. Martin-Löf’s type theory (see [Nordström et al., 1990]) provides an example of such a system, as does the Girard-Reynolds second order lambda calculus (see [Girard, 1989]). Here we will just consider a fundamental example, namely the dependently typed analogue of the algebraic theories of Section 2. So types and terms will be built up from a signature of function symbols which now may be type-valued as well as term-valued. Once one has explained the categorical framework corresponding to such dependently typed algebraic theories ^{1}, one can use it systematically to describe the categorical structure needed for any particular dependently-typed datatype constructor—much as we did for simple types in Section 3. We will just consider a single example of this, namely the categorical semantics of dependent products in Section 6.5.

Several different, but interconnected, categorical structures have been proposed for interpreting the basic framework of dependent types by Seely [1984], Cartmell [1986], Taylor [1986], Ehrhard [1988], Streicher [1989, 1991], Hyland and Pitts [1989], Obtułowicz [1989], Curien [1989], and Jacobs [1991]. This reflects the fact that the categorical interpretation of dependent types is undoubtedly more complicated than the other varieties of categorical logic explained in this chapter. This is due to the structural complications implicit in the logic. One complication is that in general one must consider the satisfaction of equations not only between terms (of the same type), but also between types. Another complication is that proofs of well-formedness of expressions cannot be separated from proofs of equality, and are by no means unique. If one assigns meanings to expressions by induction on the derivation of their well-formedness, one therefore has to take care that the meaning is independent of the particular derivation. Early accounts [Seely, 1984] of the categorical semantics of dependent types tended to gloss over this point. Here we will take a more careful, but necessarily more complicated approach using an adaptation of Cartmell’s notion of ‘category with attributes’—a simplified version of the ‘contextual categories’ he uses in [Cartmell, 1986]. Categories with attributes are categories equipped with some extra structure for interpreting (dependent) types: accordingly we adopt (in Definition 6.3.3) the rather more compact terminology of ‘type-categories’ for the categorical structure we use.

1Cartmell [1986] calls such theories ‘generalized algebraic’.

In order to motivate the notion of type-category, we will reverse the pattern set by Sects 2 and 4: having described the syntax, we will organize it into a category just as in Section 4.2, and see how the extra structure needed for a type-category emerges. We then give the interpretation of the syntax in a general type-category. The soundness of the interpretation (Theorem 6.4.5) relies on some ‘strictness’ conditions built into the definition of type-category to avoid the potential difficulties mentioned above to do with multiple proofs of well-formedness of judgements. The wide range of examples of type-categories which we give shows that these strictness conditions are not restrictive in practice. Without them one must resolve quite complicated coherence problems: see [Curien, 1990].

6.1 Syntactic considerations

We will continue to make use of the simply typed metalanguage introduced at the beginning of Section 3, with ground arities Types and Terms. We assume given a signature, Sg, consisting of collections of meta-constants

• s : Terms^{n} ↠ Types, called n-ary type-valued function symbols • F : Terms^{n} ↠ Terms, called n-ary term-valued function symbols

for each number n. The raw^{2} expressions of the object language over Sg are then the meta-expressions built up from the symbols in Sg and a fixed, countably infinite set Var = {v_{1}, v_{2}, …} of meta-variables of arity Terms. In particular, the raw types over Sg are meta-expressions of arity Types and the raw terms over Sg are meta-expressions of arity Terms. (The algebraic signatures of Sect 2.1 also contained typing information for the function symbols. The analogous information here will given as part of the axioms of a dependently-typed algebraic theory, rather than as part of its underlying signature.) Throughout Section 6, Sg will denote a fixed signature in the above sense.

2The adjective ‘raw’ is used to emphasize that not all expressions will be ‘well-formed’ in the technical sense to be explained.

Definition 6.1.1. As before, a context, Γ, is a finite list Γ = [x_{1} : σ_{1}, …, x_{n} : σ_{n}] of (variable,type)-pairs, but now subject to the following conditions on variables: for each i = 1, …, n

var(σ_{i}) ⊆ {x_{1}, …, x_{i−1}} and x_{i} ∉ {x_{1}, …, x_{i−1}}

where var(e) denotes the (finite) set of variables occurring in the expression e. Thus the variables x_{i} are distinct and each type σ_{i} only involves variables which have already been listed in the context. Notational conventions for contexts will be as in Section 2.1; in particular, [ ] denotes the empty context.

The variant of dependently typed Equational Logic that we are going to describe contains rules for deriving a number of different forms of judgement, set out in Table 1. The ‘secondary’ judgement forms are so-called because they are in fact expressible in terms of the primary forms, modulo the rules for dependently typed equational logic given below (cf. Remark 6.1.4).

Definition 6.1.2. A dependently typed algebraic theory , Th, over the signature Sg is specified by the following data.

• For each type-valued function symbol s a judgement

s(x⃗) type [Γ_{s}]

called the introductory axiom of s. Here x⃗ is the list of variables of the context Γ_{s}, and must have length n when s has arity Terms^{n} ↠ Types. Γ_{s} lists the types of the argument to which s may be applied.

• For each term-valued function symbol F a judgement

F (x⃗) : σ_{F} [Γ_{F}]

called the introductory axiom of F. Once again, x⃗ is the list of variables of the context Γ_{F}, and must have length n when F has arity Terms^{n} ↠ Terms. Γ_{F} lists the types of the arguments to which F may be applied, and σ_{F} gives the type of the result (which may depend upon those arguments).

• A collection of judgements of the form M = M′ : σ [Γ], called the term-equality axioms of Th.

• A collection of judgements of the form σ = σ′ [Γ], called the typeequality axioms of Th.

Given such a theory, the theorems of Th are the judgements which are provable using the rules shown in Figs 9 and 10. In the rules, x⃗ is the list of variables of context Γ and x′ is the list of variables of context Γ′; and supposing γ = [M_{1}, …, M_{n}] and x⃗ = [x_{1}, …, x_{n}], then σ[γ/x⃗] denotes the result of simultaneously substituting the term M_{i} for the variable x_{i}

Table 1. Forms of judgement

(Γ and Γ′ are contexts, σ and σ′ are raw types, M and M′ are raw terms, and γ and γ′ are finite lists of raw terms.)

Judgement  Intended meaning  Restriction

Primary forms

σ type [Γ] ‘σ is a well-formed type in context Γ’

var(σ) ⊆ var(Γ)

M : σ [Γ] ‘M is a well-formed term of type σ in context Γ’

var(M, σ) ⊆ var(Γ)

σ = σ′ [Γ] ‘σ and σ′ are equal (well-formed) types in context Γ’

var(σ, σ′) ⊆ var(Γ)

M = M′ : σ [Γ] ‘M and M′ are equal (well-formed) terms of type σ in context Γ’

var(M, M′, σ) ⊆ var(Γ)

Secondary forms

Γ ctxt ‘Γ is a well-formed context’

γ : Γ→Γ′ ‘γ is a context morphism from Γ to Γ′’

var(γ) ⊆ var(Γ)

Γ = Γ′ ‘Γ and Γ′ are equal (wellformed) contexts’

Γ and Γ′ of equal length

γ = γ′ : Γ→Γ′ ‘γ and γ′ are equal context morphisms from Γ to Γ′’ var(γ, γ′) ⊆ var(Γ) and γ, γ′, and Γ′ of equal length 66 Andrew M. Pitts

Contexts

[ ] ctxt σ type [Γ] ; [Γ, x : σ] ctxt
[ ] = [ ]  {Γ = Γ′ σ = σ′[x⃗/x′] [Γ] \atop [Γ, x : σ] = [Γ′, x′ : σ′]}

Types

{σ type [Γ] \atop σ = σ [Γ]} {σ = σ′ [Γ] \atop σ′ = σ [Γ]} {σ = σ′ [Γ] σ′ = σ′′ [Γ] \atop σ = σ′′ [Γ]}
γ : Γ′→Γ σ type [Γ]
σ[γ/x⃗] type [Γ′]

{γ = γ′ : Γ′→Γ σ = σ′ [Γ] \atop σ[γ/x⃗] = σ′[γ′/x⃗] [Γ′]}

Terms

[Γ, x : σ, Γ′] ctxt x : σ [Γ, x : σ, Γ′]

{M : σ [Γ] σ = σ′ [Γ] \atop M : σ′ [Γ]} {M = M′ : σ [Γ] σ = σ′ [Γ] \atop M = M′ : σ′ [Γ]}

{M : σ [Γ] \atop M = M : σ [Γ]} {M = M′ : σ [Γ] \atop M′ = M : σ [Γ]} {M = M′ : σ [Γ] M′ = M′′ : σ [Γ] \atop M = M′′ : σ [Γ]}
{γ : Γ′→Γ M : σ [Γ] \atop M[γ/x⃗] : σ[γ/x⃗] [Γ′]}  {γ = γ′ : Γ′→Γ M = M′ : σ [Γ] \atop M[γ/x⃗] = M′[γ′/x⃗] : σ[γ/x⃗] [Γ′]}

Context morphisms

{[Γ] ctxt \atop [ ] : Γ→[ ]}

γ : Γ′→Γ σ type [Γ] M : σ[γ/x⃗] [Γ′]

[γ, M] : Γ′→[Γ, x : σ]

{[Γ] ctxt \atop [ ] = [ ] : Γ→[ ]} γ = γ′ : Γ′→Γ σ type [Γ] M = M′ : σ[γ/x⃗] [Γ′]

[γ, M] = [γ′, M′] : Γ′→[Γ, x : σ]

Fig. 9. General rules

Γ_{s} ctxt

(s has introductory axiom s(x⃗) type [Γ_{s}])

s(x⃗) type [Γ_{s}]

σ_{F} type [Γ_{F}]

(F has introductory axiom F (x⃗) : σ_{F} [Γ_{F}])

F (x⃗) : σ_{F}
M : σ [Γ] M′ : σ [Γ]

(M = M′ : σ [Γ] is a term-equality axiom)

M = M′ : σ [Γ]

σ type [Γ] σ′ type [Γ]

(σ = σ′ [Γ] is a type-equality axiom).

σ = σ′ [Γ]

Fig. 10. Rules for axioms

in the type σ. In reading the rules, it should not be forgotten that we only consider contexts which are well-formed, in the sense of satisfying the conditions on variables mentioned in Definition 6.1.1. Thus for example, in the rule for deriving [Γ, x : σ], it is necessarily the case that x is distinct from the variables in Γ.

The rules in Fig. 9 are general rules for dependently typed equational logic, whereas those in Fig. 10 relate to the particular axioms of Th. Note that these rules for using the axioms of Th do have hypotheses: if the hypotheses of such a rule are never satisfied, then we can never make use of the axiom.

Definition 6.1.3. We will say that a dependently typed algebraic theory Th is well-formed if all of the hypotheses of the rules for introducing axioms are provable from the rules in Figs 9 and 10. (In this case each of the axioms is indeed a theorem of Th).

Remark 6.1.4. The form of judgement ‘ γ : Γ→Γ′ ’ is not usually made explicit in presentations of theories of dependent types. We have chosen to make it a ‘first-class’ judgement form because it permits a conceptually clear and concise formulation of the substitution rules, and because it will play a key role in the definition of the classifying category of a dependentlytyped algebraic theory in the next section. However, it is easy to see from the rules in Fig. 9 that this form of judgement, along with the forms ‘ γ = γ′ : Γ→Γ′ ’, ‘ Γ ctxt ’ and ‘ Γ = Γ′ ’, are all equivalent to finite conjunctions of instances of the forms ‘ σ type [Γ] ’, ‘ M : σ [Γ] ’, ‘ σ = σ′ [Γ] ’, and ‘ M = M′ : σ [Γ] ’.

Example 6.1.5. The theory of categories provides an example of a wellformed, dependently-typed algebraic theory. The underlying signature is:

obj : Types
hom : Terms^{2}→Types
Id : Terms→Terms
Comp : Terms^{5}→Terms.

The axioms are as follows obj type [ ]

hom(x, y) type [x : obj , y : obj ]

Id(x) : hom(x, x) [x : obj ]

Comp(x, y, z, f, g) : hom(x, z) [Γ]

Comp(x, x, y, Id(x), f) = f : hom(x, y) [x : obj, y : obj, f : hom(x, y)]

Comp(x, y, y, f, Id(y)) = f : hom(x, y) [x : obj, y : obj, f : hom(x, y)]

Comp(x, y, w, f, Comp(y, z, w, g, h)) =
Comp(x, z, w, Comp(x, y, z, f, g), h) : hom(x, w) [Δ]

where

Γ =^{def} [x : obj, y : obj, z : obj, f : hom(x, y), g : hom(y, z)]
Δ =^{def} [x : obj, y : obj, z : obj, w : obj,
f : hom(x, y), g : hom(y, z), h : hom(z, w)] .

It is evident from this example that the formal requirement in the introductory axiom of a function symbol (such as that for Comp) that all variables in the context occur explicitly as arguments of the function is at variance with informal practice. See [Cartmell, 1986, Section 10] for a discussion of this issue.

Remark 6.1.6 (Substitution and Weakening.). A general rule for substituting along a context morphism is derivable from the rules in Figs 9 and 10, viz:

γ : Γ′→Γ J [Γ] ; . ; J[γ/x⃗] [Γ′]  (6.1)

where J is one of the four forms ‘ e type ’, ‘ e = e′ ’, ‘ e : e′ ’, or ‘ e = e′ : e′′ ’, and y⃗ is the list of variables in Γ′. A special case of this is a general derived rule for weakening contexts: σ type [Γ] J [Γ, Γ′]

.

J [Γ, x : σ, Γ′]

(6.2)

The rules for substitution in Fig. 9 also have as special cases forms which correspond more closely to the substitution rule (2.9) for simply typed equational logic, viz:

{M = M′ : σ [Γ] N = N′ : τ [Γ, x : σ, Γ′] \atop N[M/x] = N′[M′/x] : τ[M/x] [Γ, Γ′[M/x]]}  (6.3)

M = M′ : σ [Γ] τ = τ′ [Γ, x : σ, Γ′] ; . ; τ[M/x] = τ′[M′/x] [Γ, Γ′[M/x]]  (6.4)

6.2 Classifying category of a theory

We are now going to construct a category, Cℓ(Th), out of the syntax of a dependently typed algebraic theory Th. In fact the construction is essentially just as in Section 4.2. More accurately, the construction in that section is the special case of the one given here when the theory has only 0-ary type-valued function symbols.

We will use the following terminology with respect to the judgements which are theorems of Th. Say that Γ is a Th-context if the judgement [Γ] ctxt is a theorem of Th; say that Th-contexts Γ and Γ′ are Th-provably equal if the judgement Γ = Γ′ is a theorem of Th; say that γ : Γ→Γ′ is a morphism of Th-contexts if the judgement γ : Γ→Γ′ is a theorem of Th; and finally, say that two Th-context morphisms are Th-provably equal if γ = γ′ : Γ→Γ′ is a theorem of Th.

Objects of Cℓ(Th). The collection of objects of the classifying category is the quotient of the set of Th-contexts by the equivalence relation of being Th-provably equal. This definition makes sense because the following rules are derivable from those in Figs 9 and 10.

{Γ ctxt \atop Γ = Γ}  {Γ = Γ′ \atop Γ′ = Γ}  Γ = Γ′ Γ′ = Γ′′ ; . ; Γ = Γ′′

We will tend not to distinguish notationally between a Th-context and the object of Cℓ(Th) that it determines.

Morphisms of Cℓ(Th). Given two objects in Cℓ(Th), represented by Thcontexts Γ and Γ′ say, the collection of morphisms in the classifying category from the first object to the second is the quotient of the set of Thcontext morphisms Γ→Γ′ by the equivalence relation of being Th-provably equal. This definition makes sense because the following rules are derivable from those in Figs 9 and 10.

Γ = Γ′ γ : Γ′→Γ′′ Γ′′ = Γ′′′
γ : Γ→Γ′′′

{γ : Γ→Γ′ \atop γ = γ : Γ→Γ′}  {γ = γ′ : Γ→Γ′ \atop γ′ = γ : Γ→Γ′}
γ = γ′ : Γ→Γ′ γ′ = γ′′ : Γ→Γ′
.
γ = γ′′ : Γ→Γ′

We will tend not to distinguish notationally between a Th-context morphism and the morphism of Cℓ(Th) which it determines.

Composition in Cℓ(Th). Given context morphisms γ : Γ→Γ′ and γ′ : Γ′→Γ′′, with γ′ = [N_{1}, …, N_{m}] and var(Γ′) = x′ say, define the composition γ′ ∘ γ : Γ→Γ′′ just as in Section 4.2, viz:

γ′ ∘ γ =^{def} [N_{1}[γ/x′], …, N_{m}[γ/x′]] .

The derived rules for substitution mentioned in Remark 6.1.6 can be used to show that the following derived rules for composition are valid.

{γ : Γ→Γ′ γ′ : Γ′→Γ′′ \atop γ′ ∘ γ : Γ→Γ′′}

{γ_{1} = γ_{2} : Γ→Γ′ γ′_{1} = γ′_{2} : Γ′→Γ′′ \atop γ′_{1} ∘ γ_{1} = γ′_{2} ∘ γ_{2} : Γ→Γ′′}

γ : Γ→Γ′ γ′ : Γ′→Γ′′ γ′′ : Γ′′→Γ′′′

.

γ′′ ∘ (γ′ ∘ γ) = (γ′′ ∘ γ′) ∘ γ : Γ→Γ′′′

From these rules it follows that a well-defined and associative operation of composition is induced on the morphisms of the classifying category. The identity morphisms for this composition are induced by the identity context morphisms id_{Γ} : Γ→Γ, which are defined just as in Section 4.2:

id_{Γ} =^{def} [x_{1}, …, x_{n}]

where x_{1}, …, x_{n} are the variables listed in Γ. These context morphisms do induce morphisms in Cℓ(Th) which are units for composition because the following rules are derivable.

Γ ctxt ; id_{Γ} : Γ→Γ
Γ = Γ′
id_{Γ} = id′_{Γ} : Γ→Γ

{γ : Γ→Γ′ \atop γ ∘ id_{Γ} = γ : Γ→Γ′}  γ : Γ→Γ′ ; . ; id′_{Γ} ∘ γ = γ : Γ→Γ′

This completes the definition of Cℓ(Th) as a category. We now move on to examine what extra categorical structure it possesses.

6.3 Type-categories

For a simply typed algebraic theory, we saw in Section 4 that the relevant categorical structure on the corresponding classifying category was finite products. Here it will turn out to be the more general^{3} property of possessing a terminal object and some pullbacks. To explain which pullbacks, we identify a special class of morphisms in the classifying category of Th.

Definition 6.3.1. If Γ is a Th-context, the collection of Γ-indexed types in Cℓ(Th) is defined to be the quotient of the set of types σ such that σ type [Γ] is a theorem of Th, with respect to the equivalence relation identifying σ and σ′ just in case σ = σ′ [Γ] is a theorem of Th. As usual, we will not make a notational distinction between σ and the Γ-indexed type it determines. Each such Γ-indexed type has associated with it a projection morphism, represented by the context morphism

π_{σ} =^{def} [x_{1}, …, x_{n}] : [Γ, x : σ]→Γ.

Here x_{1}, …, x_{n} are the variables listed in Γ, and x is any other variable. Note that the object in Cℓ(Th) represented by [Γ, x : σ] and the morphism represented by π_{σ} are independent of which particular variable x is chosen.

Lemma 6.3.2. Given a morphism γ : Γ′ ⟶ Γ in Cℓ(Th) and a Γ-indexed type represented by σ, then

[figure: [Γ′, y : σ[γ/x⃗]]; [γ, y]; [Γ, x : σ]; Γ′; π_{σ[γ/x⃗]}; γ; Γ; π_{σ}]

is a pullback square in Cℓ(Th).

Proof. Suppose given γ′ : Γ′′→Γ′ and γ′′ : Γ′′→[Γ, x : σ] in Cℓ(Th) satisfying γ ∘ γ′ = π_{σ} ∘ γ′′ : Γ′′→Γ. We have to prove that there is a unique morphism δ : Γ′′→[Γ′, x′ : σ[γ/x⃗]] satisfying π_{σ[γ/x⃗]} ∘ δ = γ′ : Γ′′→Γ′ and [γ, x′] ∘ δ = γ′′ : Γ′′→[Γ, x : σ].

3Since finite products can be constructed from pullbacks and a terminal object.

Now since γ ∘ γ′ = π_{σ} ∘ γ′′ : Γ′′→Γ, we must have that the list of terms γ′′ is of the form [γ ∘ γ′, N] for some term N for which N : σ[γ ∘ γ′/x⃗] [Γ′′] is a theorem of Th. Now since σ[γ ∘ γ′/x⃗] = σ[γ/x⃗][γ′/x′] (where x′ is the list of variables in Γ′), we get a morphism

δ =^{def} [γ′, N] : Γ′′→[Γ′, x′ : σ[γ/x⃗]]

satisfying

[γ, x′] ∘ δ = [γ, x′] ∘ [γ′, N]
= [γ ∘ γ′, N]
= γ′′

and

π_{σ[γ/x⃗]} ∘ δ = [x′] ∘ [γ′, N]
= γ′

as required. If δ′ : Γ′′→[Γ′, x′ : σ[γ/x⃗]] were any other such morphism, then from the requirement π_{σ[γ/x⃗]} ∘ δ′ = γ′ we conclude that the list δ′ is of the form [γ′, N′]; and then from the requirement [γ, x′] ∘ δ′ = γ′′ we conclude further that

N′ = N : σ[γ/x⃗][γ′/x′] [Γ′′]

is a theorem of Th, so that δ′ = δ : Γ′′→[Γ′, x′ : σ[γ/x⃗]].

The above Lemma motivates the following definition, which is essentially Cartmell’s (unpublished) notion of ‘category with attributes’.

Definition 6.3.3. A type-category, C, is a category possessing a terminal object, 1, and equipped with the following structure:

• For each object X in C, a collection Type_{C}(X), whose elements will be called X-indexed types in C.

• For each object X in C, operations assigning to each X-indexed type A an object X ⋉ A, called the total object of A, together with a morphism

π_{A} : X ⋉ A ⟶ X

called the projection morphism of A.

• For each morphism f : Y ⟶ X in C, an operation assigning to each X-indexed type A, a Y indexed type f^{∗}A, called the pullback of A along X, together with a morphism f ⋉ A : Y ⋉ f^{∗}A ⟶ X ⋉ A making the following a pullback square in the category C.

[figure: Y ⋉ f^{∗}A; f ⋉ A; X ⋉ A; Y; π_{f^{∗}A}; f; X; π_{A}]  (6.5)

In addition, the following strictness conditions will be imposed on these operations:

id_{X}^{∗}A = A and id_{X} ⋉ A = id_{X⋉A}

g^{∗}(f^{∗}A) = (f ∘ g)^{∗}A and (f ⋉ A) ∘ (g ⋉ f^{∗}A) = (f ∘ g) ⋉ A .

Notation 6.3.4. If C is a type-category and X is a C-object, then as usual C/X will denote the slice category whose objects are the C-morphisms with codomain X, f : dom(f) ⟶ X, and whose morphisms f ⟶ f′ are C-morphisms g : dom(f) ⟶ dom(f′) satisfying f′ ∘ g = f. Identity morphisms and composition in C/X are inherited from those in C. Note that for each A ∈ Type_{C}(X), the projection morphism π_{A} is an object in the slice category C/X. So we can make Type_{C}(X) into a category (equivalent to a full subcategory of C/X) by taking morphisms A ⟶ A′ to be C/Xmorphisms π_{A} ⟶ π_{A′} (with identities and composition inherited from C/X).

Proposition 6.3.5. The classifying category, Cℓ(Th), of a dependently typed algebraic theory Th is a type-category.

Proof. We identified notions of indexed type and associated projection morphisms for Cℓ(Th) in Definition 6.3.1 and verified in Lemma 6.3.2 the existence of pullback squares of the required form (6.5). The ‘strictness’ conditions in Definition 6.3.3 are met because of the usual properties of substitution of terms for variables. Finally, note that Cℓ(Th) does have a terminal object, namely the (equivalence class of the) empty context [ ].

Here are some examples of ‘naturally-occurring’ type-categories.

Example 6.3.6 (Sets). The category Set of sets and functions supports the structure of a type-category: for each set X, we can take the X-indexed types to be set-valued functions with domain X. Given such a function A : X ⟶ Set, the associated total set is the disjoint union

X ⋉ A =^{def} _{∐x∈X}A(x) = {(x, a) | x ∈ X & a ∈ A(x)}

with projection function π_{A} given by first projection (x, a) ↦ x.

The pullback of A along a function f : Y ⟶ X is just the composition

f^{∗}A =^{def} A ∘ f : Y ⟶ Set

which indeed results in a pullback square in Set of the required form (6.5) and satisfying the strictness conditions, with f ⋉ A : Y ⋉ f^{∗}A ⟶ X ⋉ A equal to the function (y, a) ↦ (f(y), a).

Note the following property of this example, which is not typical of typecategories in general: up to bijection over X, any function with codomain X, f : Y ⟶ X, can be expressed as the projection function associated with an indexed type:

f = (Y ≅^{i} X ⋉ A ⟶^{π_{A}} X)

where A(x) = {y ∈ Y | f(y) = x} and i(y) = (f(y), y).

Example 6.3.7 (Constant families). Every category C with finite products can be endowed with the structure of a type-category, in which the indexed types are ‘constant families’. For each object X in C, one defines Type_{C}(X) to be Obj_{C}, the class of all objects of C. The associated operations are

X ⋉ A =^{def} X × A  (categorical product)
π_{A} =^{def} π_{1} : X × A ⟶ X (first projection).

Given f : Y ⟶ X in C and A ∈ Type_{C}(X) = Obj_{C}, the pullback Y -indexed type f^{∗}A is just the object A itself and the morphism f ⋉ A : Y ⋉ f^{∗}A ⟶ X ⋉ A is f × id_{A}. This does yield a pullback square in C, viz.:

[figure: Y × A; f × id_{A}; X × A; Y; π_{1}; f; X; π_{1}]

and these pullbacks do satisfy the strictness conditions in Definition 6.3.3. When a category with finite products is regarded as a type-category in this way, the categorical semantics of simply typed algebraic theories given in Section 2 becomes essentially a special case of the semantics of dependently typed theories to be given below.

Example 6.3.8 (Toposes). The following example is given for readers familiar with the notion of topos (see the references in Section 7). One can make each topos E into a type-category as follows. First note that E is indeed a category with a terminal object. For each object X ∈ Obj_{E}, define Type_{E}(X) to consist of all pairs (A, a) where A ∈ Obj_{E} and a : X ×A ⟶ Ω. Here Ω denotes the codomain of the object classifier of E, ⊤ : 1 ⟶ Ω. Given such an X-indexed type, the total object X ⋉ (A, a) is given by forming a pullback square in E:

[figure: X ⋉ (A, a); X × A; 1; ⊤; Ω; a]  (6.6)

The projection morphism associated to (A, a) is defined by the composition

π_{(A,a)} : X ⋉ (A, a) ⟶ X × A ⟶^{π_{1}} X .

For any morphism f : Y ⟶ X, f^{∗}(A, a) is defined to be the Y -indexed type (A, a ∘ (f × id_{A})). The pullback square (6.5) is obtained as the factorization through (6.6) of the corresponding pullback for a ∘ (f × id_{A}). Elementary properties of pullback squares ensure that the strictness conditions of Definition 6.3.3 hold, without the need for any coherence assumptions on the chosen pullback operations for E. Traditionally, dependently typed theories have been interpreted in toposes using the locally cartesian closed structure that they possess, whereby the category Type_{E}(X) of X-indexed types (cf. 6.3.4) is just the slice category E/X: see [Seely, 1984]. Such a choice for indexed types yields a ‘non-strict’ type-category structure, in that the strictness conditions of Definition 6.3.3 have to be weakened by replacing the equalities by coherent isomorphisms. This can lead to complications in the interpretation of type theory: see [Curien, 1990]. The method of regarding a topos as a type-category given here achieves the strictness conditions and side-steps issues of coherence. Given that toposes correspond to theories in intuitionistic higher order logic (cf. [Bell, 1988], [Mac Lane and Moerdijk, 1992]), this example can form the basis for interpreting dependently typed theories in higher order predicate logic: see [Jacobs and Melham, 1993]. However, Hofmann [1995] has recently pointed out that using a particular construction of Bénabou (for producing a split fibration equivalent to a given fibration), an arbitrary locally cartesian closed category, E, can be endowed with a more involved notion of X-indexed type which makes E a type-category (supporting the interpretation of product, sum and identity types) and with Type_{E}(X) equivalent to E/X (pseudonaturally in X).

Example 6.3.9 (Split fibrations). Let Cat denote the category of small categories and functors. We can turn it into a type-category by decreeing that for each small category, C, the C-indexed types are functors A : C^{op} ⟶ Cat. The associated total category C⋉A is given by a construction due to Grothendieck:

• An object of C ⋉ A is a pair (X, A), with X an object of C and A an object of A(X).

• A morphism in C ⋉ A from (X, A) to (X′, A′) is a pair (x, a), where x : X ⟶ X′ in C and a : A ⟶ A(x)(A′) in A(X). The composition of two such morphisms (x, a) : (X, A) ⟶ (X′, A′) and (x′, a′) : (X′, A′) ⟶ (X′′, A′′) is given by the pair (x′ ∘ x, A(x)(a′) ∘ a). The identity morphism for the object (X, A) is given by (id_{X}, id_{A}).

The projection functor πA : C⋉A ⟶ C is of course given on both objects and morphisms by projection onto the first co-ordinate.

The pullback of the indexed type A : C^{op} ⟶ Cat along a functor F : D ⟶ C is just given by composing A with F, regarded as a functor D^{op} ⟶ C^{op}. Applying the Grothendieck construction to A and to A ∘ F, one obtains a pullback square in the category Cat of the required form, with F ⋉ A : D ⋉ (A ∘ F) ⟶ C ⋉ A the functor which acts on objects and morphisms by applying F in the first co-ordinate.

Regarding a set as a discrete category, there is an inclusion between the type-category of Example 6.3.6 and the present one. Unlike the previous example, not every morphism in Cat arises as the first projection of an indexed type. Those that do were characterized by Grothendieck and are known as ‘split Grothendieck fibrations’. As the name suggests, these are a special instances of the more general notion of ‘Grothendieck fibration’— which would give a more general way of making Cat into a type-category, except that the ‘strictness’ conditions in Definition 6.3.3 are not satisfied. See [Jacobs, 1991] for more information on the use of Grothendieck fibrations in the semantics of type theory.

6.4 Categorical semantics

We will now give the definition of the semantics of the types, terms, contexts and context morphisms of Th in a type-category C. In general contexts are interpreted as C-objects, context morphisms as C-morphisms, and types as indexed types in C. Terms as interpreted using the following notion of ‘global section’ of an indexed type.

Definition 6.4.1. Given an object X in a type-category C, the global sections of an X-indexed type A ∈ Type_{C}(X) are the morphisms a : X ⟶ X ⋉ A in C satisfying π_{A} ∘ a = id_{X}. We will write

a ∈_{X} A

to indicate that a is a global section of the X-indexed type A. For any morphism f : Y ⟶ X, using the universal property of the pullback square (6.5) we get

f^{∗}a ∈_{Y} f^{∗}A

where f^{∗}a : Y ⟶ Y ⋉ f^{∗}A is the unique morphism with π_{f^{∗}A} ∘ f^{∗}a = id_{Y} and (f ⋉ A) ∘ f^{∗}a = a ∘ f.

Definition 6.4.2. Let Sg be a signature as in Section 6.1. A structure for Sg in a type-category C is specified by:

• For each type-valued function symbol s, a C-object X_{s} and an indexed type A_{s} ∈ Type_{C}(X_{s}).

• For each term-valued function symbol F, a C-object X_{F}, an indexed type A_{F} ∈ Type_{C}(X_{F}), and a global section a_{F} ∈_{X_{F}} A_{F}.

Semantics of expressions. Given such a structure, we will define four relations:

[[Γ ctxt]] ≍ X
[[σ type [Γ]]] ≍ A [X]
[[M : σ [Γ]]] ≍ a : A [X]
[[γ : Γ′→Γ]] ≍ f : X′→X

where the judgements enclosed by [[ ]] are all well-formed and where X is a C-object, A ∈ Type_{C}(X), a ∈_{X} A, and f is a morphism from X′ to X in C. These relations are defined inductively by the rules in Fig. 11. In the first rule concerning context morphisms, ⟨ ⟩ : X→1 denotes the unique morphism from X to the terminal object. The two rules concerning the semantics of variables use the following pairing notation.

Notation 6.4.3. Referring to the pullback square (6.5), if g : Z ⟶ Y and h : Z ⟶ X ⋉ A are morphisms satisfying f ∘ g = π_{A} ∘ h, then

⟨g, h⟩ : Z ⟶ Y ⋉ f^{∗}A

will denote the unique morphism satisfying π_{f^{∗}A} ∘ ⟨g, h⟩ = g and (f ⋉ A) ∘ ⟨g, h⟩ = h whose existence is guaranteed by the universal property of the pullback square. Thus for example, in this notation the global section f^{∗}a ∈_{Y} f^{∗}A referred to in Definition 6.4.1 is given by the morphism ⟨id_{Y} , a∘ f⟩ : Y ⟶ Y ⋉ f^{∗}A.

It is clear from the form of the rules in Fig. 11 that the relations they define are monogenic, in the sense that for a judgement J and categorical structures E and E′, if [[J]] ≍ E and [[J]] ≍ E′, then E = E′ in C. Thus given a structure for Sg in C, the assignments 78 Andrew M. Pitts

Contexts [[[ ] ctxt]] ≍ 1

[[Γ ctxt]] ≍ X [[σ type [Γ]]] ≍ A [X]

[[[Γ, x : σ] ctxt]] ≍ X ⋉ A Types

{[[γ : Γ→Γ_{s}]] ≍ f : X→X_{s} \atop [[s(γ) type [Γ]]] ≍ f^{∗}A_{s} [X]}

Terms

[[Γ ctxt]] ≍ X [[σ type [Γ]]] ≍ A [X] [[τ type [Γ, x : σ]]] ≍ π_{A}^{∗}A [X ⋉ A]

[[x : τ [Γ, x : σ]]] ≍ ⟨id_{X⋉A}, id_{X⋉A}⟩ : π_{A}^{∗}A [X ⋉ A]

[[Γ ctxt]] ≍ X [[σ type [Γ]]] ≍ A [X] [[σ′ type [Γ, x : σ]]] ≍ A′ [X ⋉ A]

[[τ type [Γ, x : σ, x′ : σ′]]] ≍ (π_{A′} ∘ π_{A})^{∗}A [X ⋉ A ⋉ A′] [[x : τ [Γ, x : σ, x′ : σ′]]] ≍ ⟨id_{X⋉A⋉A′}, π_{A′}⟩ : (π_{A′} ∘ π_{A})^{∗}A [X ⋉ A ⋉ A′]

[[γ : Γ→Γ_{F}]] ≍ f : X→X_{F} [[σ type [Γ]]] ≍ f^{∗}A_{F} [X]

[[F (γ) : σ [Γ]]] ≍ f^{∗}a_{F} : f^{∗}A_{F} [X]

Context morphisms

{[[Γ ctxt]] ≍ X \atop [[[ ] : Γ→[ ]]] ≍ ⟨ ⟩ : X→1}

[[γ : Γ′→Γ]] ≍ f : X′→X [[σ type [Γ]]] ≍ A [X]

[[M : σ[γ/x⃗] [Γ′]]] ≍ a : f^{∗}A [X′]

[[[γ, M] : Γ′→[Γ, x : σ]]] ≍ (f ⋉ A′) ∘ a : X′→X ⋉ A Fig. 11. Categorical semantics

Γ ↦ [[Γ ctxt]]
σ, Γ ↦ [[σ type [Γ]]]
M, σ, Γ ↦ [[M : σ [Γ]]]
γ, Γ′, Γ ↦ [[γ : Γ′→Γ]]

determine partial functions. We will write [[J]]⇓ to indicate that these partial functions are defined at a particular argument J.

Remark 6.4.4. The case when J is x : τ [Δ] deserves some comment, since this is the most complicated case in the definition of [[J]]. The wellformedness of x : τ [Δ] guarantees that x is assigned a type in Δ, i.e. that Δ is of the form [Γ, x : σ, Γ′]. However, the presence of type equality judgements in the logic means that σ is not necessarily syntactically identical to τ. This accounts for the presence of the hypotheses concerning τ in the two rules for this case in Fig. 11. The first of these two rules deals with the case when Γ′ = [ ], and then the second rule must be applied repeatedly to deal with general Γ′.

Satisfaction of judgements Next we define what it means for the various forms of judgement to be satisfied by a structure for Sg in a type-category, C.

• Γ ctxt is satisfied if and only if [[Γ ctxt]]⇓.

• σ type [Γ] is satisfied if and only if [[σ type [Γ]]]⇓.

• M : σ [Γ] is satisfied if and only if [[M : σ [Γ]]]⇓.

• γ : Γ→Γ′ is satisfied if and only if [[γ : Γ→Γ′]]⇓.

• Γ = Γ′ is satisfied if and only if for some (necessarily unique) object

X [[Γ ctxt]] ≍ X and [[Γ′ ctxt]] ≍ X .

• σ = σ′ [Γ] is satisfied if and only if for some (necessarily unique) object X and X-indexed type A ∈ Type_{C}(X)

[[σ type [Γ]]] ≍ A [X] and [[σ′ type [Γ]]] ≍ A [X] .

• M = M′ : σ [Γ] is satisfied if and only if for some (necessarily unique) object X, indexed type A ∈ Type_{C}(X), and global section a ∈_{X} A

[[M : σ [Γ]]] ≍ a : A [X] and [[M′ : σ [Γ]]] ≍ a : A [X] .

• γ = γ′ : Γ→Γ′ is satisfied if and only if for some (necessarily unique) morphism f : X′ ⟶ X in C

[[γ : Γ′→Γ]] ≍ f : X′→X and [[γ′ : Γ′→Γ]] ≍ f : X′→X .

Suppose Th is a dependently typed algebraic theory. A model of Th in a type-category, C, is a structure in C for the underlying signature of Th with the property that the collection of judgements satisfied by the structure is closed under the rules for the axioms of Th given in Fig. 10.

Theorem 6.4.5 (Soundness). The collection of judgements that are satisfied by a structure in a type-category, C, is closed under the general rules of dependently typed equational logic given in Fig. 9. Consequently, a model in C of a dependently typed algebraic theory, Th, satisfies all the judgements which are theorems of Th.

Much as with the corresponding result for simply typed equational logic, the key tool used in proving the above theorem is a lemma giving the behaviour of substitution in the categorical semantics:

Lemma 6.4.6 (Semantics of substitution). Suppose that [[γ : Γ′→Γ]] ≍ f : X′→X. Then

[[σ type [Γ]]] ≍ A [X] ⇒ [[σ[γ/x⃗] type [Γ′]]] ≍ f^{∗}A [X′]
[[M : σ [Γ]]] ≍ a : A [X] ⇒ [[M[γ/x⃗] : σ[γ/x⃗] [Γ′]]] ≍ f^{∗}a : f^{∗}A [X′]
[[γ′ : Γ′′→Γ′]] ≍ f′ : X′′→X′ ⇒ [[γ ∘ γ′ : Γ′′→Γ]] ≍ f ∘ f′ : X′′→X .

The generic model of a well-formed theory. Suppose that Th is a dependently typed algebraic theory that is well-formed, in the sense of Definition 6.1.3. Then the classifying category Cℓ(Th) contains a structure, G, for the underlying signature of Th. G is defined as follows, where we use a notation for the components of the structure as in Definition 6.4.2.

The well-formedness of Th implies that for each type-valued function symbol s, with introductory axiom s(x⃗) type [Γ_{s}] say, Γ_{s} is a Th-context and hence determines an object X_{s} of Cℓ(Th). Then define the X_{s}-indexed type A_{s} ∈ Type_{Cℓ(Th)}(X_{s}) to be that represented by s(x⃗) (which is a Γ_{s}- indexed type because s(x⃗) type [Γ_{s}] is a theorem of Th).

For each term-valued function symbol F with introductory axiom F (x⃗) : σ_{F} [Γ_{F}], the well-formedness of Th implies that σ_{F} type [Γ_{F}] is a theorem of Th. Hence Γ_{F} is a Th-context and hence determines an object X_{F} =^{def} Γ_{F} of Cℓ(Th). Then define the X_{F} -indexed type A_{F} ∈ Type_{Cℓ(Th)}(X_{F}) to be that represented by the Γ_{F} -indexed type σ_{F}, and define the global section a_{F} ∈_{X_{F}} A_{F} to be the morphism X_{F} ⟶ X_{F} ⋉ A_{F} in Cℓ(Th) represented by the Th-context morphism [id_{Γ_{F}} , F (x⃗)] : Γ_{F} ⟶ [Γ_{F} , x : σ_{F}].

The structure G has the following properties:

• For each judgement Γctxt and Cℓ(Th)-object X, the relation [[Γ]] ≍ X holds if and only if Γ ctxt is a theorem of Th and X is the object of Cℓ(Th) represented by Γ.

• For each judgement σ type [Γ], each object X and each X-indexed type A ∈ Type_{Cℓ(Th)}(X), the relation [[σ type [Γ]]] ≍ A [X] holds if and only if σ type [Γ] is a theorem of Th, X is the object of Cℓ(Th) represented by Γ, and A is the X-indexed type represented by σ.

• For each judgement M : σ [Γ], each object X and each X-indexed type A ∈ Type_{Cℓ(Th)}(X), and each global section a ∈_{X} A, the relation [[M : σ [Γ]]] ≍ a ∈ A [X] holds if and only if X is the object of Cℓ(Th) represented by Γ, A is the X-indexed type represented by σ, and a is the global section represented by the Th-context morphism [id_{Γ}, M] : Γ ⟶ [Γ, x : σ].

• An equality judgement is satisfied by G if and only if it is a theorem of Th.

Thus G is a model of Th and a judgement is satisfied by this model if and only if it is a theorem of Th.

Remark 6.4.7. The classifying type-category Cℓ(Th) and the generic model G of a well-formed, dependently typed algebraic theory Th have a universal property analogous to that given for algebraic theories in Theorem 4.2.5, with respect to a suitable notion of morphism of type-categories. To go further and develop a correspondence between dependently typed algebraic theories and type-categories along the lines of Section 4.3, one has to restrict to the subclass of ‘reachable’ type-categories. For note that an object X in a type-category C can appear as the interpretation of a context only if for some n ≥ 0 there is a sequence of indexed types

A_{1} ∈ Type_{C}(1), A_{2} ∈ Type_{C}(1 ⋉ A_{1}), …, A_{n} ∈ Type_{C}(1 ⋉ A_{1} ⋉ ⋯ ⋉ A_{n−1})

with X = 1 ⋉ A_{1} ⋉ ⋯ ⋉ A_{n}. Call C reachable if there is such a sequence for every C-object. Every classifying category has this property. Conversely if C is reachable, then it is equivalent to Cℓ(Th) for a theory in a suitable ‘internal language’ for C (cf. Section 2.3).

6.5 Dependent products

The categorical framework corresponding to dependently typed equational logic that we have given can be used to infer the categorical structure needed for various dependently typed datatype constructors—much as we did for simple types in Section 3. We will just consider one example here, namely the structure in a type-category corresponding to dependent products. The formation, introduction, elimination, and equality rules for dependent product types are given in Fig. 12. Equality rules for both β- and η-conversion are given. There are also congruence rules for the constructors Π, λ, and ap, which we omit (cf. Remark 3.0.3).

If C is a type-category, the existence of the pullback squares (6.5) allows us to define a functor between slice categories

π_{A}^{∗} : C/X ⟶ C/(X ⋉ A)  (6.7)

given by pullback along π_{A} : X ⋉ A ⟶ X:

σ type [Γ] σ′(x) type [Γ, x : σ]

Π(σ, σ′) type [Γ]

{M′(x) : σ′(x) [Γ, x : σ] \atop λ(M′) : Π(σ, σ′) [Γ]}

{N : Π(σ, σ′) [Γ] M : σ [Γ] \atop ap(N, M) : σ′(M) [Γ]}

{M′(x) : σ′(x) [Γ, x : σ] M : σ [Γ] \atop ap(λ(M′), M) = M′(M) : σ′(M) [Γ]}

{N : Π(σ, σ′) [Γ] \atop N = λ((x)ap(N, x)) : Π(σ, σ′) [Γ]}

Fig. 12. Rules for dependent product types

π_{A}^{∗} (f ^{g} f′) =^{def} (f ⋉ A ^{⟨g∘π_{f^{∗}A},f⋉A⟩} f′ ⋉ A) .

(This definition makes use of the pairing notation introduced in 6.4.3.) Symmetrically, there is a functor

f^{∗} : Type_{C}(X) ⟶ Type_{C}(Y)  (6.8)

induced by pullback along f : Y ⟶ X:

f^{∗} (A ^{g} A′) =^{def} (f^{∗}A ^{⟨π_{f^{∗}A},g∘(f⋉A)⟩} f^{∗}A′) .

Definition 6.5.1. A type-category C has dependent products if for each X ∈ Obj_{C}, A ∈ Type_{C}(X), and A′ ∈ Type_{C}(X ⋉ A), there is an indexed type

Π(A, A′) ∈ Type_{C}(X)  (6.9)

and a morphism in Type_{C}(X ⋉ A)

ap_{A,A′} : π_{A}^{∗}Π(A, A′) ⟶ A′  (6.10)

satisfying:

• Adjointness Property. π_{Π(A,A′)} : X ⋉ Π(A, A′) ⟶ X is the value of the right adjoint to the pullback functor (6.7) at π_{A′} : X ⋉A⋉A′ ⟶ X ⋉ A, with counit ap_{A,A′}. In other words, for any f : Y ⟶ X in C and g : π_{A}^{∗}(f) ⟶ π_{A′} in C/(X ⋉ A), there is a unique morphism in C/X

cur(g) : f ⟶ π_{Π(A,A′)}

satisfying ap_{A,A′} ∘ π_{A}^{∗}(cur(g)) = g.

• Strictness Property. For any morphism f : Y ⟶ X in C:

f^{∗}Π(A, A′) = Π(f^{∗}A, (f ⋉ A)^{∗}A′)
(f ⋉ A)^{∗}(ap_{A,A′}) = ap_{f^{∗}A,(f⋉A)^{∗}A′}

Here f^{∗} and (f ⋉ A)^{∗} are instances of the pullback functors (6.8).

To specify the categorical semantics of dependent product types in such a type-category, we give rules extending the inductively defined relation of Section 6.4.

Formation

[[σ type [Γ]]] ≍ A [X] [[σ′(x) type [Γ, x : σ]]] ≍ A′ [X ⋉ A]
[[Π(σ, σ′) type [Γ]]] ≍ Π(A, A′) [X]

(6.11)

Introduction

[[σ type [Γ]]] ≍ A [X] [[σ′(x) type [Γ, x : σ]]] ≍ A′ [X ⋉ A]
[[M′(x) : σ′(x) [Γ, x : σ]]] ≍ a′ : A′ [X ⋉ A]
[[λ(M′) : Π(σ, σ′) [Γ]]] ≍ cur(a′) : Π(A, A′) [X]

(6.12)

Note that the conclusion of this rule is well-formed if the hypotheses are. For if a′ ∈_{X⋉A} A′, then a′ : π_{A}^{∗}(id_{X}) = id_{X⋉A} ⟶ π_{A′} in C/X ⋉ A; so we can apply the Adjointness Property from Definition 6.5.1 to form cur(a′) : id_{X} ⟶ π_{Π(A,A′)}, which is in particular a global section of Π(A, A′).

Elimination

[[σ type [Γ]]] ≍ A [X] [[σ′(x) type [Γ, x : σ]]] ≍ A′ [X ⋉ A]

[[N : Π(σ, σ′) [Γ]]] ≍ b : Π(A, A′) [X] [[M : σ [Γ]]] ≍ a : A [X]

[[ap(N, M) : σ′(M) [Γ]]] ≍ ⟨id_{X} , ap_{A,A′} ∘ ⟨a, b⟩⟩ : a^{∗}A′ [X]

(6.13)

If the hypotheses of this rule are well-formed, then a ∈_{X} A and b ∈_{X} Π(A, A′), i.e. a : id_{X} ⟶ π_{A} and b : id_{X} ⟶ π_{Π(A,A′)} in C/X. Since π_{A} ∘ a = id_{X} = π_{Π(A,A′)} ∘ b, we can use the pairing operation of 6.4.3 to form

⟨a, b⟩ : X ⟶ X ⋉ A ⋉ π_{A}^{∗}Π(A, A′) .

Since by definition π_{π_{A}^{∗}Π(A,A′)} ∘ ⟨a, b⟩ = a, we get a morphism ⟨a, b⟩ : a ⟶ π_{π_{A}^{∗}Π(A,A′)} in C/(X ⋉ A) and hence by composition a morphism ap_{A,A′} ∘ ⟨a, b⟩ : a ⟶ π_{A′}. Since A ∘ id_{X} = a = π_{A′} ∘ ap_{A,A′} ∘ ⟨a, b⟩, the pairing operation yields a morphism

⟨id_{X} , ap_{A,A′} ∘ ⟨a, b⟩⟩ : X ⟶ X ⋉ a^{∗}A

whose composition with π_{a^{∗}A′} is id_{X} and hence which is a global section of a^{∗}A′. Thus the conclusion of the above rule is well-formed when its hypotheses are.

With these rules we can extend Theorem 6.4.5 to include dependent product types.

Theorem 6.5.2 (Soundness). Defining satisfaction of judgements as in Section 6.4, it is the case that the collection of judgements satisfied by a structure in a type-category with dependent products is closed under the rules in Fig. 12 (as well as the general rules of Fig. 9).

Thus the structure of Definition 6.5.1 is sufficient for soundly interpreting dependent products. On the other hand it is necessary, in the sense that Proposition 6.3.5 can be extended as follows.

Proposition 6.5.3. If Th is a theory in dependently typed equational logic with dependent product types, then the classifying category Cℓ(Th) constructed in Section 6.2 is a type-category with dependent products.

Proof. Referring to Definition 6.5.1, to define (6.9) find judgements

Γ ctxt  σ type [Γ]  σ′(x) type [Γ, x : σ]

that are theorems of Th and such that X, A, and A′ are the equivalence classes of Γ, σ, and σ′(x) respectively. Then take Π(A, A′) to be the Γindexed type determined by Π(σ, σ′). This definition is independent of the choice of representatives. The morphism (6.10) is that represented by the Th-context morphism

[id_{Γ}, x, ap(z, x)] : [Γ, x : σ, z : Π(σ, σ′)] ⟶ [Γ, x : σ, x′ : σ(x)] .

Since π_{σ′(x)}∘[id_{Γ}, x, ap(z, x)] = id_{[Γ,x:σ]} this does indeed induce a morphism of the required kind; and once again the definition of ap_{A,A′} is independent of the choice of representatives.

The Adjointness Property required for Π(A, A′) can be deduced from the equality rules in Fig. 12, and the Stability Property follows from standard properties of substitution.

7 Further Reading

This section lists some important topics in categorical logic which have not been covered in this chapter and gives pointers to the literature on them.

Higher order logic The study of toposes (a categorical abstraction of key properties of categories of set-valued sheaves) and their relationship to set theory and higher order logic has been one of the greatest stimuli of the development of a categorical approach to logic. [Mac Lane and Moerdijk, 1992] provides a very good introduction to topos theory from a mathematical perspective; [Lambek and Scott, 1986, Part II] and [Bell, 1988] give accounts emphasizing the connections with logic. The hyperdoctrine approach to first order logic outlined in Section 5 can be extended to higher order logic and such higher order hyperdoctrines can be used to generate toposes: see [Hyland et al., 1980], [Pitts, 1981], [Hyland and Ong, 1993].

Polymorphic lambda calculus Hyperdoctrines have also been used successfully to model type theories involving type variables and quantification over types. [Crole, 1993, Chps 5 and 6] provides an introduction to the categorical semantics of such type theories very much in the spirit of this chapter.

Categories of relations Much of the development of categorical logic has been stimulated by a process of abstraction from the properties of categories of sets and functions. However, categorical properties of sets and binary relations (under the usual operation of composition of relations) have also been influential. The book by Freyd and Scedrov [1990] provides a wealth of material on categorical logic from this perspective.

Categorical proof theory Both Lawvere [1969] and Lambek [1968] put forward the idea that proofs of logical entailment between propositions, ϕ ⊢ ψ, may be modelled by morphisms, [[ϕ]] ⟶ [[ψ]], in categories. If one is only interested in the existence of such proofs, then one might as well only consider categories with at most one morphism between any pair of objects, i.e. only consider pre-ordered sets. This is the point of view taken in Section 5. However, to study the structure of proofs one must consider categories rather than just pre-orders. Lambek in particular has studied the connection between this categorical view of proofs and the two main styles of proof introduced by Gentzen (Natural Deduction and Sequent Calculus), introducing the notion of multicategory to model sequents in which more than one proposition occurs on either side of the turnstile, ⊢ : see [Lambek, 1989]. This has resulted in applications of proof theory to category theory, for example in the use of cut elimination theorems to prove coherence results: see [Minc, 1977], [Mac Lane, 1982]. In the reverse direction of applications of category theory to proof theory, general categorical machinery, particularly enriched category theory, has provided useful guidelines for what constitutes a model of proofs in Girard’s Linear Logic (see [Seely, 1989], [Barr, 1991], [Mackie et al., 1993], [Bierman, 1994]); for example in [Benton et al., 1993], such considerations facilitated the discovery of a well-behaved Natural Deduction formulation of intuitionistic linear logic.

Categorical combinators The essentially algebraic nature of the category theory corresponding to various kinds of logic and type theory gives rise to var¡iable-free, combinatory presentations of such systems. These have been used as the basis of abstract machines for expression evaluation and type checking: see [Curien, 1993], [Ritter, 1992].

References

[Backhouse et al., 1989] R. Backhouse, P. Chisholm, G. Malcolm, and E. Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1:19–84, 1989.

[Barr and Wells, 1990] M. Barr and C. Wells. Category Theory for Com-

puting Science. Prentice Hall, 1990. [Barr, 1991] M. Barr. ∗-autonomous categories and linear logic. Math.

Structures in Computer Science, 1:159–178, 1991. [Bell, 1988] J. L. Bell. Toposes and Local Set Theories. An Introduction,

volume 14 of Oxford Logic Guides. Oxford University Press, 1988. [Benton et al., 1993] P. N. Benton, G. M. Bierman, V. C. V. de Paiva, and

J. M. E. Hyland. A term calculus for intuitionistic linear logic. In Bezem and Groote [1993], pages 75–90.

[Bezem and Groote, 1993] M. Bezem and J. F. Groote, editors. Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1993.

[Bierman, 1994] G. M. Bierman. On Intuitionistic Linear Logic. PhD

thesis, Cambridge Univ., 1994. [Bloom and Ésik, 1993] S. L. Bloom and Z. Ésik. Iteration Theories.

EATCS Monographs on Theoretical Computer Science. Springer-Verlag, New York, 1993.

[Cartmell, 1986] J. Cartmell. Generalised algebraic theories and contextual

categories. Annals of Pure and Applied Logic, 32:209–243, 1986. [Chang and Keisler, 1973] C. C. Chang and H. J. Keisler. Model Theory.

North-Holland, Amsterdam, 1973. [Coste, 1979] M. Coste. Localisation, spectra and sheaf representation. In

M. P. Fourman, C. J. Mulvey, and D. S. Scott, editors, Applications of Sheaves, volume 753 of Lecture Notes in Mathematics, pages 212–238. Springer-Verlag, Berlin, 1979.

[Crole and Pitts, 1992] R. L. Crole and A. M. Pitts. New foundations for fixpoint computations: Fix-hyperdoctrines and the fix-logic. Information and Computation, 98:171–210, 1992.

[Crole, 1993] R. L. Crole. Categories for Types. Cambridge Univ. Press, [Curien, 1989] P.-L. Curien. Alpha-conversion, conditions on variables and

categorical logic. Studia Logica, 48:319–360, 1989. [Curien, 1990] P.-L. Curien. Substitution up to isomorphism. Tech-

nical Report LIENS-90-9, Laboratoire d’Informatique, Ecole Normale Supérieure, Paris, 1990.

[Curien, 1993] P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Birkhäuser, Boston, 1993. Second Edition.

[Dummett, 1977] M. Dummett. Elements of Intuitionism. Oxford Univer-

sity Press, 1977. [Ehrhard, 1988] Th. Ehrhard. A categorical semantics of Constructions. In

3rd Annual Symposium on Logic in Computer Science, pages 264–273. IEEE Computer Society Press, Washington, 1988.

[Freyd and Scedrov, 1990] P. J. Freyd and A. Scedrov. Categories, Alle-

gories. North-Holland, Amsterdam, 1990. [Freyd, 1972] P. J. Freyd. Aspects of topoi. Bull. Austral. Math. Soc.,

7:1–76 and 467–80, 1972. [Girard, 1986] J.-Y. Girard. The system f of variable types, fifteen years

later. Theoretical Computer Science, 45:159–192, 1986. [Girard, 1987] J.-Y. Girard. Linear logic. Theoretical Computer Science,

50:1–102, 1987. [Girard, 1989] J.-Y. Girard. Proofs and Types, volume 7 of Cambridge

Tracts in Theoretical Computer Science. Cambridge University Press, 1989. Translated and with appendices by Paul Taylor and Yves Lafont.

[Goguen and Meseguer, 1985] J. A. Goguen and J. Meseguer. Initiality, induction and computability. In Nivat and Reynolds [1985], pages 459– 541.

[Goguen et al., 1977] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. JACM, 24:68–95, 1977.

[Gray and Scedrov, 1989] J. W. Gray and A. Scedrov, editors. Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics. Amer. Math. Soc, Providence RI, 1989.

[Hofmann, 1995] M. Hofmann. On the interpretation of type theory in locally cartesian closed cateories. In J. Tiuryn, editor, Computer Science Logic, Kazimierz, Poland, 1994, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1995.

[Hyland and Ong, 1993] J. M. E. Hyland and C.-H. L. Ong. Modified realizability toposes and strong normalization proofs. In Bezem and Groote [1993], pages 179–194.

[Hyland and Pitts, 1989] J. M. E. Hyland and A. M. Pitts. The theory of constructions: categorical semantics and topos-theoretic models. In

Gray and Scedrov [1989], pages 137–199. [Hyland et al., 1980] J. M. E. Hyland, P. T. Johnstone, and A. M. Pitts.

Tripos theory. Math. Proc. Cambridge Philos. Soc., 88:205–232, 1980. [Hyland, 1988] J. M. E. Hyland. A small complete category. Annals of

Pure and Applied Logic, 40:135–165, 1988. [Jacobs and Melham, 1993] B. Jacobs and T. Melham. Translating depen-

dent type theory into higher order logic. In Bezem and Groote [1993], pages 209–229.

[Jacobs, 1991] B. Jacobs. Categorical Type Theory. PhD thesis, Univ.

Nijmegen, 1991. [Lambek and Scott, 1986] J. Lambek and P. J. Scott. Introduction to

Higher Order Categorical Logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge Univ. Press, 1986.

[Lambek, 1968] J. Lambek. Deductive systems and categories i. Math.

Systems Theory, 2:287–318, 1968. [Lambek, 1988] J. Lambek. On the unity of algebra and logic. In

F. Borceux, editor, Categorical Algebra and its Applications, volume 1348 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1988.

[Lambek, 1989] J. Lambek. Multicategories revisited. In Gray and Scedrov

[1989], pages 217–239. [Lawvere, 1964] F. W. Lawvere. An elementary theory of the category of

sets. Proc. Nat. Acad. Sci. USA, 52:1506–1511, 1964. [Lawvere, 1966] F. W. Lawvere. The category of categories as a foundation

for mathematics. In S. Eilenberg et al, editor, Proc. Conference on Categorical Algebra, La Jolla, pages 1–21, 1966.

[Lawvere, 1969] F. W. Lawvere. Adjointness in foundations. Dialectica,

23:281–296, 1969. [Lawvere, 1970] F. W. Lawvere. Equality in hyperdoctrines and the com-

prehension schema as an adjoint functor. In A. Heller, editor, Applications of Categorical Algebra, pages 1–14. American Mathematical Society, Providence RI, 1970.

[Mac Lane and Moerdijk, 1992] S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic. A first introduction to topos theory. Universitext. Springer-Verlag, Berlin, 1992.

[Mac Lane, 1971] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, Berlin, 1971.

[Mac Lane, 1982] S. Mac Lane. Why commutative diagrams coincide with

equivalent proofs. Contemporary Mathematics, 13:387–401, 1982. [Mackie et al., 1993] I. Mackie, L. Román, and S. Abramsky. An inter-

nal language for autonomous categories. Applied Categorical Structures, 1:311–343, 1993.

[Makkai and Reyes, 1977] M. Makkai and G. E. Reyes. First Order Categorical Logic, volume 611 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1977.

[McLarty, 1992] C. McLarty. Elementary Categories, Elementary Toposes,

volume 21 of Oxford Logic Guides. Oxford University Press, 1992. [Minc, 1977] G. E. Minc. Closed categories and the theory of proofs. Zap.

Nauch. Sem. Leningrad. Otdel. Mat. Inst. im. V. A. Steklova (LOMI), 96:83–114,145, 1977. Russian, with English summary.

[Mitchell and Scott, 1989] J. C. Mitchell and P. J. Scott. Typed lambda models and cartesian closed categories (preliminary version). In Gray and Scedrov [1989], pages 301–316.

[Moggi, 1991] E. Moggi. Notions of computations and monads. Informa-

tion and Computation, 93:55–92, 1991. [Nivat and Reynolds, 1985] M. Nivat and J. C. Reynolds, editors. Alge-

braic Methods in Semantics. Cambridge University Press, 1985. [Nordström et al., 1990] B. Nordström, K. Petersson, and J. M. Smith.

Programming in Martin-Löf’s Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, 1990.

[Obtułowicz, 1989] A. Obtułowicz. Categorical and algebraic aspects of

martin-löf type theory. Studia Logica, 48:299–318, 1989. [Oles, 1985] F. J. Oles. Types algebras, functor categories and block struc-

ture. In Nivat and Reynolds [1985], chapter 15, pages 543–574. [Pierce, 1991] B. C. Pierce. Basic Category Theory for Computer Scien-

tists. MIT Press, 1991. [Pitts, 1981] A. M. Pitts. The Theory of Triposes. PhD thesis, Cambridge

Univ., 1981. [Pitts, 1987] A. M. Pitts. Polymorphism is set theoretic, constructively. In

D. H. Pitt, A. Poigné, and D. E. Rydeheard, editors, Category Theory and Computer Science, Proc. Edinburgh 1987, volume 283 of Lecture Notes in Computer Science, pages 12–39. Springer-Verlag, Berlin, 1987.

[Pitts, 1989] A. M. Pitts. Non-trivial power types can’t be subtypes of polymorphic types. In 4th Annual Symposium on Logic in Computer Science, pages 6–13. IEEE Computer Society Press, Washington, 1989.

[Reynolds and Plotkin, 1993] J. C. Reynolds and G. D. Plotkin. On functors expressible in the polymorphic typed lambda calculus. Information and Computation, 105:1–29, 1993.

[Reynolds, 1983] J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513–523. Elsevier B.V. (North-Holland), Amsterdam, 1983.

[Ritter, 1992] E. Ritter. Categorical Abstract Machines for Higher-Order Typed Lambda Calculi. PhD thesis, Cambridge Univ., 1992.

[Román, 1989] L. Román. Cartesian categories with natural numbers ob-

ject. Journal of Pure and Applied Algebra, 58:267–278, 1989. [Scott, 1980] D. S. Scott. Relating theories of the lambda calculus. In J. P.

Seldin and J. R. Hindley, editors, To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 403–450. Academic Press, London, 1980.

[Seely, 1984] R. A. G. Seely. Locally cartesian closed categories and type

theories. Math. Proc. Cambridge Philos. Soc., 95:33–48, 1984. [Seely, 1987] R. A. G. Seely. Categorical semantics for higher order poly-

morphic lambda calculus. Journal of Symbolic Logic, 52:969–989, 1987. [Seely, 1989] R. A. G. Seely. Linear logic, ∗-autonomous categories and

cofree algebras. In Gray and Scedrov [1989], pages 371–382. [Streicher, 1989] Th. Streicher. Correctness and Completeness of a Cate-

gorical Semantics of the Calculus of Constructions. PhD thesis, Univ. Passau, 1989. Tech. Report MIP-8913.

[Streicher, 1991] Th. Streicher. Semantics of Type Theory. Birkhäuser,

1991. [Taylor, 1986] P. Taylor. Recursive domains, indexed category theory and

polymorphism. PhD thesis, Cambridge Univ., 1986.

Subject Index

C-property, 41 Th-algebra, 9 Th-context, 69

algebraic theory, 7

dependently typed, 64 arity, 13 axiom

term-equality, 64 type-equality, 64

Beck-Chevalley condition, 58–59 bi-rule, 48

categorical combinators, 86 category

bicartesian closed, 39 cartesian closed, 24 classifying, 32 prop-, 41 slice, 73 type-, 72 well-pointed, 11 well-powered, 43

category with attributes, 63 classifying

category, 32 prop-category, 60 type-category, 69–71

coherence, 63, 85 completeness, 39, 59–62 computational lambda calculus, 27 computation type, 27 context, 6, 64

Th-provably equal, 31 α-equivalence of, 30 identity morphism, 31 morphism, 31 morphism composition, 31

contextual categories, 63

dependent product type, 82 disjoint union type, 14

element generalized, 11 global, 11 empty type, 19 equation-in-context, 7 equational logic, 7

dependently typed, 66–67 essentially algebraic, 3, 86 evaluation morphism, 24 exponential object, 24

finite product strictly associative, 33 strictly unital, 33

finite products category with, 7 preservation of, 29 strict preservation of, 30

formula atomic, 39 well-formed, 39

formula-in-context, 39 Frobenius reciprocity, 53 functionsymbol

introductory axiom, 64 function symbol, 5

introductory axiom, 64 term-valued, 63 type-valued, 63

function type, 22

generalized element, 11 generalized quantifiers, 57 generic

T h-algebra, 34

model, 39, 61, 80–81 global element, 11 global section, 76 Grothendieck fibration, 76 ground type, 13

higher order logic, 85 hyperdoctrine, 42

inclusive subset, 42 indexed type, 72 inductive type, 24 internal language, 3, 10, 57 iteration theory, 36

92 Subject Index

Linear Logic, 49, 85

meta-expression, 13 model

of a dependently typed theory,

79 of a predicate theory, 59

multicategory, 85

natural number object, 27 weak, 27

one-element-type, 21

polymorphic lambda calculus, 85 product type, 19 projection morphism, 72 Proof Theory, 85 prop-category, 41

classifying, 60

has equality, 56

has existential quantification, 53 has finite joins, 46 has finite meets, 45 has Heyting implications, 46 has universal quantification, 53

pullback of an indexed type, 73 of a property, 41

realizability, 51 relation symbol, 39 rules

adjoint style, 48, 52, 55

natural deduction style, 48, 52, 55

satisfaction of an equation, 9 of a judgement, 79 of sequent, 45

sequent, 40 signature, 5, 63 slice category, 73 sort, 5 soundness, 9 stable

coproduct, 18–19

initial object, 19

join, 49 stage, 11 strictness condition, 73 strong monad, 27 structure

for an algebraic theory, 8 for a dependently typed theory,

77 for a predicate theory, 43

subobject, 42

term-in-context, 6 term-model, 3 theory

algebraic, 7 axioms of, 7 dependently typed algebraic, 64 in predicate logic, 40 theorems of, 7, 40, 64 translation, 36

topos, 74, 85 total object, 72 type

computation, 27

dependent product, 82 disjoint union, 14 empty, 19 function, 22 ground, 13 indexed, 72 inductive, 24 one-element, 21 product, 19 type-category, 72

classifying, 69–71

has dependent products, 82 reachable, 81

weak product, 21 well-formed theory, 67 well-pointed, 11

Notation Index

(∃-Elim), 52 (=-Elim), 55 (=-Intr), 55 (&-Adj ), 48 (&-Elim_{1}), 48 (&-Elim_{2}), 48 (&-Intr), 48 (∨-Adj ), 48 (∨-Elim), 48 (∨-Intr_{1}), 48 (∨-Intr_{2}), 48 (∃-Adj), 52 (∃-Intr), 52 (false-Adj ), 48 (false-Elim), 48 (∀-Adj ), 52 (∀-Intr), 52 (⇒-Adj ), 48 (⇒-Elim), 48 (⇒-Intr), 48 (Contract), 41 (Cut), 41 (Exchange), 41 (Subst), 41 (Weaken), 41 (x)e, 13 ⟨−, …, −⟩, 7 ⟨−, −⟩, 77 =_{Th}, 31 =_{σ}, 55 A_{F}, 77 A_{s}, 77 F : σ_{1}, …, σ_{n} ⟶ τ, 5 M = M′ : σ [Γ], 65 M : σ [Γ], 65 M : σ [Γ], 6 N[M/x], 7 N[M⃗/x⃗], 8 R ⊆ σ_{1}, …, σ_{n}, 39 X ⋉ A, 72 X_{F}, 77 X_{s}, 77 T σ, 27 Cat, 76 Cℓ(Th), 32, 69 Δ_{X}, 56 Eq_{X}, 55 Γ = Γ′, 65 Γ ctxt, 65 Γ_{F}, 64 Γ_{s}, 64 0 , 19 ⋁I,X, 52 ⋁f, 57 K, 50 Kℓ, 42 let, 28 ⋀I,X, 52 ⋀f, 57 null, 19 Obj_{C}, 74 P, 50 Φ ⊢ ψ [Γ], 40 Π, 82 Π(A, A′), 82 Prop_{C}, 41 P_{1}, 50 TX, 28 S, 50 Set, 42, 73 Sg, 5 Sg_{C}, 10 1, 8 Terms, 13 Types, 13 Th_{C}, 35 Type_{C}, 72 val, 28 ap, 22, 82 ⇔, 47 ⊥_{X}, 46 case, 15 &, 47 cons, 24 ctxt, 65 δ_{X}, 56 [[M[Γ]]], 8 [[ϕ[Γ]]], 43 ∨, 47 empty_{τ}, 19 ⊢, 40 ≡, 13 η_{X}, 28

94 Notation Index

∃_{σ}, 51 false, 47 ∀_{σ}, 51 γ : Γ→Γ′, 65 γ = γ′ : Γ→Γ′, 65 →, 46 ⇒, 47 inl_{X,X′}, 15 inr_{X,X′}, 15 inl_{σ′}, 14 inr_{σ}, 14 ⇓, 50, 79 ∨, 46 ≍, 50, 77 λ, 82 λ_{σ}, 22 ≤, 41 listit, 25 listrec, 24 ⋉, 72 ap_{A,A′}, 82 ap_{X,Y}, 23 cur, 83 cur_{I}, 22 lift_{I}, 28 ∧, 45 ↠, 13 ¬, 47 nil_{σ}, 24 pair, 20 π_{A} : X ⋉ A ⟶ X, 72 π_{σ}, 71 π_{i}, 7 proj, 21 prop, 39 ⇀, 42 σ + σ′, 14 σ = σ′ [Γ], 65 σlist, 24 σ→σ′, 22 σ × σ′, 19 σ_{F}, 64 snd, 21 split, 20 ⋆, 21 ⋀, 45 ⊤_{X}, 45 true, 47 type, 65 unit, 21 {−|−}_{I}, 16 a ∈_{X} A, 76 a_{F}, 77 e(e′), 13 f ⋉ A, 73 f^{∗}A, 41, 72 n · x, 50 pr, 45 sigma type [Γ], 65 − × ⋯ × −, 7 Alg, 36 Fp, 36 LX, 24 cons_{X}, 24 listrec_{I}, 24 nil_{X}, 24 var(Γ), 6