Book Review:

Categorical Logic and Type Theory
by B. Jacobs
Studies in Logic and the Foundations of Mathematics, Vol 141, Elsevier.
ISBN: 0 444 50170 3
Review by R.A.G. Seely
(The Bulletin of Symbolic Logic Vol. 6 (2000) No. 2, pp. 225-229.)

NOTE: If the font seems "weird" anywhere on this page, please try this PDF link instead.
Test: φ should look like the Greek letter phi; σ should look like the Greek letter sigma; ω should look like the Greek letter omega; λ should look like the Greek letter lambda; ∈ should look like a stylized epsilon (actually, the "element" relation symbol); ⊢ should look like a "turnstile" (or "vdash"); and → should look like a right arrow.

This is a book on logic, type theory, and proof theory. It should not be overlooked by any potential reader who focuses only on the word "categorical". Of course, it has a natural constituency among categorical logicians and theoretical computer scientists interested in various type theories. But a book such as this addresses issues of fundamental importance, not merely for categorical logicians, but more importantly also for more "traditional" type theorists and proof theorists, who are in danger of missing its message.

Since the late 1960's there has been considerable progress in understanding the algebraic semantics of logic and type theory, particularly because of the development of categorical analyses of most of the structures of interest to logicians. Although there have been other algebraic approaches to logic, none has been as far reaching in its aims and in its results as the categorical approach has been. From fairly modest beginnings, categorical logic has matured very nicely in the past three decades; the book presently under review is good evidence of that process.

Many readers of this journal will probably be acquainted with the connections between typed lambda calculus and Cartesian closed categories, and between intuitionist set theory and toposes, as outlined e.g. in the book Introduction to higher order categorical logic by J. Lambek and P.J. Scott (1986). They may also be familiar with the now classic work on categorical logic by M. Makkai and G.E. Reyes (First order categorical logic, 1977). Some readers may also know that such correspondences exist between other logics and/or type theories and appropriate categorical doctrines, for instance, Martin-Löf's dependant types, or polymorphic lambda calculus, to mention but two. But what has been most striking in the past decade and a half is the degree to which such work, and much that has been done since, has been given a more unified treatment using the technical notion of fibrations. Jacobs develops a strikingly wide amount of material with this unifying notion, and presents the tools necessary for a deep understanding of the algebraic structure of the logics and type theories we are likely to consider.

"A logic is always a logic over a type theory." This is Jacobs' guiding principal, describing a type theory as a theory of types over which a logic lives. He might also say that a type theory is (often) the proof theory of a logic, under what is generally known as the Curry-Howard "proposition-as-types" isomorphism. So the treatment of logic in this book is intimately tied to the treatment of type theory. In both cases, the main technical device used is the notion of a fibration. The semantics of type theory may be presented in several ways, but any attempts to give it an algebraic formulation in suitably general terms are bound to converge on a fibrational approach. Since this notion is so fundamental to this approach, let us spend a moment to consider what is involved.

One aspect of logic is that it deals with variables, of various types. Certain operations do not essentially alter the set of free variables involved, (e.g. forming the meet or join of formulas), but others (such as quantification) do have an essential effect. There are also many type theories involving types with variables (such as dependant type theories or polymorphic type theories); these have a similar structure. To properly take variables into consideration, some notion of "indexing" is necessary. Consider for instance the simplest example: multisorted predicate logic. A formula φ(x) with a free variable x of type X may be thought to be indexed by X - think of φ (x) as an X-indexed collection of "objects" φx. One can imagine richer examples of this phenomenon: e.g. a type might depend on term variables, which in turn could have types which depend on term variables of previously constructed types. For example, one might have a subtype N(k) of the natural numbers from 1 to k, for a natural number kN. In a similar vein, one might consider the type of lists (of some type) of a fixed length k, the type of integers mod k, the type of vectors in Rk, or even (given a k and a vector v: Rk) the type of linear transformations RkRk that send v to 0, the zero vector. In short, examples of such dependency are to be found throughout ordinary mathematics and computer science. So the "index types" can have quite a rich structure themselves.

Fibrations provide precisely the kind of structure necessary for such indexing. There are other notions, but fibrations provide serious technical advantages. Apart from matters of theoretical elegance, one of the most significant advantages is perhaps the ability to treat logics (and type theories) in a modular fashion. This is illustrated throughout the book, but nowhere quite as strikingly as in the last couple of chapters which deal with notions of dependant type theories: extensions of predicate logic over simple type theory, e.g. logic over dependant types or over polymorphic types, may be dealt with by treating the logic as a "module" over the appropriate type theory.

There are two fairly obvious ways one could treat "indexing": thinking of sets and functions for the moment, we can regard an indexed family of sets {Xi | iI } either as a map X: IX, so that X(i) = Xi and X is (or contains) the collection of the Xi, or as a map X: XI, so that X -1(i) = Xi and X is the disjoint union of the Xi (where X(x) is the index of the set to which x belongs). The first approach leads to the notion of "indexed category", and has the advantage that initially it seems more intuitive and technically simpler; its main conceptual drawback is that it places the emphasis on the individual "fibres" Xi. The second approach, which emphasizes the global entity that represents the family of sets, leads to the notion of fibration. It has the advantage that it avoids the axiom of choice in places where it really is unnecessary, and so permits the description of canonical constructions; essentially, this means that the principal notions of importance are properties of a structure, rather than being additional structure. Also fibrations make the modular approach mentioned above much more straightforward. For example, if a logic is given by a fibration "above" a type theory, and the type theory itself involves variables (e.g. types may have term or type variables), then the type theory is itself a fibration, and the overall structure of the logic over the type theory is just a fibration over a fibration. The ability to compose fibrations makes this approach to semantics technically more flexible and more powerful; it is the essence of this algebraic approach to type theory and proof theory, and compared to it, other approaches often seem contrived. This is particularly true where dependencies are made over dependencies, as with polymorphic and dependent types, but even with logics over simple type theory (for instance) the fibrational approach allows a unity of view that is not achieved with a more traditional treatment.

The theory of fibrations goes back to work of Grothendieck (Catégories fibrées et descente, SGA1, 1960/61, published in Springer Lecture Notes in Mathematics 224, 1971), but in the early 1970's, Jean Benabou and his students realized its significance for foundational studies, particularly for the foundations of category theory (The journal of symbolic logic, 50 (1985) 10-37). Right from the start, it was realized that "in many domains of mathematics we have important notions of `families', e.g. vector bundles, homotopies, families of analytic manifolds ... but the family is the global entity ... Why should the emphasis be on the fibres ... ?" One might well add type theories and logics to this list: if anything, the need to stack one structure on top of another is even more pronounced in logic, and so the need for this global algebraic structure to simplify and modularize the semantics is more striking. The research on the fibrational approach to type theory and logic in the past decade and a half, culminating in the present book, offers a sound justification of this viewpoint.

Jacobs gives a thorough account of the semantics of several type theories and of logics over these. His pattern of exposition is quite consistent: he starts with a concrete description of the theory or logic at hand, in a manner that would be familiar to most logicians, and then introduces abstraction as needed, always with clear motivation. For example, the reasons for using fibrations as an organizing device will be clear to the reader well before the technicalities arise.

Jacobs' experience as a computer scientist and as a logician makes him sensitive to the amount of care that is necessary in presenting logical systems. He pays considerable attention to the minutiae of syntax, without belaboring the point, seeking the right level of syntactic precision. The text can be read at an informal level which may help the beginner get the gist of the matter, but when careful attention to detail becomes necessary, the reader does not have to work this out from careless prose, but rather can depend on the author's care in getting the details right the first time.

One of the strong points of this book is its potential pedagogical value as a graduate text. It covers a very wide range of topics, touching upon virtually all the standard topics in (categorical) logic, proof theory, type theory, and model theory. Of course, to cover so wide a range, many topics are merely introduced, but references to the extensive bibliography allow a student to follow up on topics of interest. This book ought to help make more logicians aware of the value of the fibrational approach to semantics; were it to succeed in that alone, it would have served a useful purpose. Some experience with elementary category theory and logic are probably necessary prerequisites for reading this book, and so this would be best for a second semester graduate course.

Rather than systematically go through the table of contents (which the reader may do on the publisher's web site), let me describe some key topics covered by Jacobs' book. Initially, he gives an introduction to the theory of fibrations, motivated particularly by the notions of indexing and substitution. A number of concrete examples not only illustrate the notions being developed, but will later be crucial in describing the semantics of such structures as simple type theory and dependant type theory. The following chapters cover the basic semantics of simple type theory, equational logic, first order and higher order predicate logic. Much of classical "categorical logic" is handled (at least briefly) in these chapters, all covered here from the uniform perspective given by fibrations. For example, regular and exact categories, toposes, etc. are characterized as categories whose subobject fibrations satisfy evident logical axioms, or equivalently, which have appropriate structure and properties. He introduces the notion of functorial semantics (the insight that a model is a structure preserving functor, for the appropriate notion of structure for the logic being considered), and extends it to the fibrational context so he can handle the various logics and type theories being considered. In these chapters, one can see one of the virtues of the fibered approach: one can have several different logics suitable for some structure; this just amounts to having different fibrations over the same base. In his 1985 article (op. cit.), Benabou made the point that equality is a structure an entity ("set", "category" ...) may or may not carry; implicit in this is the notion that such an entity may in fact carry several different notions of equality. As a simple example, consider the category Rel of sets and relations. We may regard a relation as a "multifunction" (a function with many outputs for a single input). Such multifunctions have several reasonable notions of equality: e.g. R = S if and only if R(x) = S(x) for any x, or e.g. R = S if and only if R(x) and S(x) have elements in common (are not disjoint). These different notions of equality "live in" different fibrations built on top of Rel.

In the chapter on higher order predicate logic Jacobs introduces the notion of a "generic object", that will prove to be central to the semantics of polymorphic type theory. Let's consider the more familiar setting of higher order logic: in order to quantify over propositions and predicates, we may use a type Prop of propositions, with an axiom PropType. There is a bijection between predicates x:σ ⊢ φ: Prop with a free variable of type σ, and terms φ: σ → Prop. We may say that Prop is a "generic object". Given abstractly, this is the necessary extra ingredient to a first order fibration over a Cartesian closed base in order to make it higher order. Jacobs goes on in later chapters to use this to give suitable functorial semantics for logic over dependant types and over polymorphic types.

In Chapter 9, Jacobs returns to the theory of fibrations, in order to develop the more sophisticated tools that will be necessary to handle dependant types. He starts by showing that there is a close connection between "global" structure (products, coproducts, Cartesian closed structure) and "fibred" structure (such structure over each index). At times the precise conditions for a "good" correspondence are somewhat subtle, and this section needs close attention. He develops a general theory of quantification and equality in terms of comonadic structure based on weakening and contraction (though contraction is actually induced by the rest of the structure). Again, the details are sufficiently subtle that the novice reader should study the simple examples to see how this generalizes the straightforward quantification from earlier chapters. Finally he introduces "double indexing" - e.g. Prop over Type over Kind - which corresponds to having fibrations over fibrations. To do this properly one needs to develop "category theory" over a fibration. This section studies this setup, using the notions originally due to J. Benabou from the 1970's.

This material is then used to analyze dependant type theories and logic over dependant types; one famous example of this is D. Scott's closure operators on Pω; this is a λω-fibration (a fibration over higher order polymorphic type theory). A richer example is given by partial equivalence relations (symmetric, transitive, not necessarily reflexive) in the effective topos; in an earlier chapter much of the structure of the effective topos is studied, and the book ends with this famous example (in categorical logic) of a structure that models (albeit in a subtle manner) full higher order dependant type theory. One technical device worth mentioning is the notion of comprehension categories. These have a dual role: they may be interpreted as "domains of quantification", or as "models of dependant type theory", and this dual view allows a modular (or incremental) approach to the semantics (and so to the syntax, via term models) of these fully dependant type theories.

The reader of this review will have gathered by now that I like this book. It covers a vast amount of material, although it leaves even more out, so any reader familiar with the field will regret the omission of his or her favorite topics. Its bibliography and the references in the text to the bibliography do compensate to some extent, but complaints will be inevitable. However as an introductory text it is exemplary, as a reference it will prove invaluable. There is one omission that strikes me: the author is a theoretical computer scientist, who is experienced with the many applications this material has in that domain. Although there are many references in the text to such applications, very little actual development of these topics is made, and generally when such material is exposed, this is only in an introductory manner, more substantive material being referred to only bibliographically. A more subjective quibble: on a number of occasions Jacobs draws a distinction between "traditional" logic and the (categorical) logic treated by this book. For example, he says that traditional logic is single sorted, unlike the multisorted logic necessary for applications in computer science (and for categorical applications in general). In effect, he is alluding to issues that were raised, and settled mathematically, twenty to thirty years ago; that they persist is not a mathematical but rather a sociological fact, and there is no need for apology in using the more general (categorical) setting where its superiority is manifest.

There are many minor typographical errors, although very few that caused me any serious misunderstanding. Overall, the production is of a high quality (a feature that seems more due to the author than to his publisher, I think). The exercises amplify many of the topics very well, and enable the book to cover far more material than would otherwise be possible. This book will be the standard reference in its field for some time to come.

File translated from TEX with the assistance of TTH, version 2.66 (with some manual "cleaning" afterwards).