##
**Categorical logic and type theory.**
*(English)*
Zbl 0911.03001

Studies in Logic and the Foundations of Mathematics. 141. Amsterdam: Elsevier. xviii, 760 p. (1999).

The reviewer’s first reaction, on picking up this book, was to wonder what on earth the author had found to say on the subject of categorical logic and type theory that could possibly fill 760 pages. After reading the book, I wonder no longer; but the feeling remains that, if the author had been a little more selective in his choice of material to include, the result could have been a much more readable, and potentially more useful, book. To say this is not to belittle the author’s achievement in collecting and organizing a very large body of material in coherent form; however, this is first and foremost an encyclopaedic work, into which specialists will delve with much pleasure and profit, rather than a text from which students (other than the most hardy and determined ones) will readily learn how to use the material.

The author considers a wide range of different (typed) logics, beginning with simple typed lambda-calculus, and moving on to first-order and higher-order predicate logic, polymorphic type theory and finally dependent type theory. His aim is to set up a common formalism for these, and for their categorical semantics, which will be truly ‘modular’ in the computer-science sense: that is, each new feature can simply be bolted on to the existing structure as and when it is introduced. This is of course a laudable aim; but it does have the effect of making the early chapters of the book, where one is dealing with comparatively simple structures, harder to read than they might have been, because of all the ‘fastenings’ that have to be put in place for the later additions to bolt on to. The author is scrupulous about explaining the eventual purpose of all these ‘fastenings’ as he goes along, but it does not seem to the reviewer that this makes his account any easier for a beginner to follow.

The common theme of the categorical semantics is, rightly, the theory of fibred or indexed categories. At present there is a conspicuous lack of a comprehensive account of fibred category theory in the literature: category-theorists have been waiting at least two decades for Jean Bénabou’s promised account of the subject, which now seems unlikely ever to see the light of day. Contained within the present volume, there are the makings of a good book on fibred categories – not the book that Bénabou would have written, but a good book nonetheless – but, once again, it seems unlikely to serve as a textbook for students wishing to learn this material, because of the difficulty of disentangling it from the formal logical calculi which are Jacobs’ main subject of study. Nevertheless, it is good to have an account in which regular categories, coherent categories, logoses and even toposes are introduced in terms of properties of fibrations.

Of course, the topos theory is there for a specific purpose: namely to introduce the effective topos and the ‘complete small category’ of PERs within it, which is needed to provide fibrational models for the polymorphic and dependent type theories studied later in the book. The author provides a careful account of the construction and properties of this topos, which is probably the best account currently available in book form – though the reviewer was a little disappointed that the emphasis is entirely on the ‘Kleene algebra’, with almost no mention of the possibility of constructing similar toposes from other combinatory algebras.

The polymorphic and dependent type theories, which form the subject of three out of the last four chapters of the book, are primarily of interest because of their connections with the semantics of programming languages. The author provides a good and clearly written account of these connections, which (from a mathematician’s point of view) is far more thorough, and therefore more satisfying, than what one often encounters in papers written by computer scientists. But, once again, one has to wonder how many computer scientists will have the stamina to work through the 440 pages needed to reach even the first of these chapters.

One very welcome feature of the book is a comprehensive bibliography of nearly 350 items. However, in view of its length, it might have been helpful if the author had attempted to give some rough classification of the entries by type or subject-area.

The author considers a wide range of different (typed) logics, beginning with simple typed lambda-calculus, and moving on to first-order and higher-order predicate logic, polymorphic type theory and finally dependent type theory. His aim is to set up a common formalism for these, and for their categorical semantics, which will be truly ‘modular’ in the computer-science sense: that is, each new feature can simply be bolted on to the existing structure as and when it is introduced. This is of course a laudable aim; but it does have the effect of making the early chapters of the book, where one is dealing with comparatively simple structures, harder to read than they might have been, because of all the ‘fastenings’ that have to be put in place for the later additions to bolt on to. The author is scrupulous about explaining the eventual purpose of all these ‘fastenings’ as he goes along, but it does not seem to the reviewer that this makes his account any easier for a beginner to follow.

The common theme of the categorical semantics is, rightly, the theory of fibred or indexed categories. At present there is a conspicuous lack of a comprehensive account of fibred category theory in the literature: category-theorists have been waiting at least two decades for Jean Bénabou’s promised account of the subject, which now seems unlikely ever to see the light of day. Contained within the present volume, there are the makings of a good book on fibred categories – not the book that Bénabou would have written, but a good book nonetheless – but, once again, it seems unlikely to serve as a textbook for students wishing to learn this material, because of the difficulty of disentangling it from the formal logical calculi which are Jacobs’ main subject of study. Nevertheless, it is good to have an account in which regular categories, coherent categories, logoses and even toposes are introduced in terms of properties of fibrations.

Of course, the topos theory is there for a specific purpose: namely to introduce the effective topos and the ‘complete small category’ of PERs within it, which is needed to provide fibrational models for the polymorphic and dependent type theories studied later in the book. The author provides a careful account of the construction and properties of this topos, which is probably the best account currently available in book form – though the reviewer was a little disappointed that the emphasis is entirely on the ‘Kleene algebra’, with almost no mention of the possibility of constructing similar toposes from other combinatory algebras.

The polymorphic and dependent type theories, which form the subject of three out of the last four chapters of the book, are primarily of interest because of their connections with the semantics of programming languages. The author provides a good and clearly written account of these connections, which (from a mathematician’s point of view) is far more thorough, and therefore more satisfying, than what one often encounters in papers written by computer scientists. But, once again, one has to wonder how many computer scientists will have the stamina to work through the 440 pages needed to reach even the first of these chapters.

One very welcome feature of the book is a comprehensive bibliography of nearly 350 items. However, in view of its length, it might have been helpful if the author had attempted to give some rough classification of the entries by type or subject-area.

Reviewer: P.T.Johnstone (Cambridge)

### MSC:

03-02 | Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations |

03G30 | Categorical logic, topoi |

03B15 | Higher-order logic; type theory (MSC2010) |

18B25 | Topoi |

18D30 | Fibered categories |

68Q55 | Semantics in the theory of computing |