**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.)

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 *k*
∈ **N**. 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 **R**^{k}, or even (given a *k* and a
vector **v**: **R**^{k}) the type of linear
transformations **R**^{k} → **R**^{k} 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 {*X*_{i} | *i*
∈ *I* } either as a map
*X*: *I* → **X**,
so that *X*(*i*) = *X*_{i} and **X**
is (or contains) the collection of the *X*_{i},
or as a map *X*: **X** → *I*,
so that *X*^{ -1}(*i*) = *X*_{i}
and **X** is the disjoint union of
the *X*_{i} (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"
*X*_{i}. 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 **Prop** ⊢ **Type**. 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 T