jacobs1999-categorical-logic

Abstract

Categorical Logic and Type Theory by Bart Jacobs is a detailed account of the categorical structures underlying logic, type theory, and semantics. The book develops the mathematical machinery needed to understand how logical systems can be interpreted in categories, moving from basic categorical logic through fibrations, indexed categories, comprehension, regular and coherent logic, higher-order logic, dependent type theory, and polymorphism. A central theme is that logic is not merely syntax with rules, but can be studied through its invariant semantic structure: predicates as fibres, substitution as reindexing, quantifiers as adjoints, and type formers as categorical constructions.

The book is valuable as a bridge between categorical logic and the semantics of dependent type theory. Jacobs presents type theory through fibrational and indexed-categorical methods, making precise how contexts, types, terms, equality, substitution, and logical structure interact. Rather than focusing only on elementary topoi or purely syntactic presentations, the book gives a broad framework in which many logical systems can be compared. It is a substantial reference work, best read selectively, but it remains one of the standard sources for understanding the categorical semantics of type theory, higher-order logic, and their connections to computer science.

Outline

0. Prospectus

0.1. Logic, type theory, and fibred category theory

Usin the terminology:

Simple type theory (STT) - $λ_{\to}$ - Simply-Typed Lambda Calculus
Polymorphic type theory (PTT) - $λ 2$
Dependent type theory - $λ P$
Higher-order type theory - $λ C$
0.2. The logic and type theory of sets

2. Simple type theory

2.1. The basic calculus of types and terms
2.2. Functorial semantics
2.3. Exponents, products and coproducts
2.4. Semantics of simple type theories
2.5. Semantics of the untyped lambda calculus as a corollary
2.6. Simple parameters

3. Equational Logic

3.1. Logics
3.2. Specifications and theories in equational logic
3.3. Algebraic specifications
3.4. Fibred equality
3.5. Fibrations for equational logic
3.6. Fibred functorial semantics

4. First order predicate logic

4.1. Signatures, connectives and quantifiers
4.2. Fibrations for first order predicate logic
4.3. Functorial interpretation and internal language
4.4. Subobject fibrations I: regular categories
4.5. Subobject fibrations II: coherent categories and logoses
4.6. Subset types
4.7. Quotient types
4.8. Quotient types, categorically
4.9. A logical characterisation of subobject fibrations

5. Higher order predicate logic

5.1. Higher order signatures
5.2. Generic objects
5.3. Fibrations for higher order logic
5.4. Elementary toposes
5.5. colimits, power objects and well-poweredness in a topos
5.6. Nuclei in a topos
5.7. Separated objects and sheaves in a topos
5.8. A logical description of separated objects and sheaves

6. The effective topos

6.1. Constructing a topos from a higher order fibration
6.2. The effective topos and its subcategories of sets, u;-sets, and PERs
6.3. Families of PERs and u;-sets over the effective topos
6.4. Natural numbers in the effective topos and some associated principles

7. Internal category theory

7.1. Definition and examples of internal categories
7.2. Internal functors and natural transformations
7.3. Externalisation
7.4. Internal diagrams and completeness

8. Polymorphic type theory

8.1. Syntax
8.2. Use of polymorphic type theory
8.3. Naive set theoretic semantics
8.4. Fibrations for polymorphic type theory
8.5. Small polymorphic fibrations
8.6. Logic over polymorphic type theory

9. Advanced fibred category theory

9.1. Opfibrations and fibred spans
9.2. Logical predicates and relations
9.3. Quantification
9.4. Category theory over a fibration
9.5. Locally small fibrations
9.6. Definability

10. First order dependent type theory

10.1. A calculus of dependent types
10.2. Use of dependent types
10.3. A term model
10.4. Display maps and comprehension categories
10.5. Closed comprehension categories
10.6. Domain theoretic models of type dependency

11. Higher order dependent type theory

11.1. Dependent predicate logic
11.2. Dependent predicate logic, categorically
11.3. Polymorphic dependent type theory
11.4. Strong and very strong sum and equality
11.5. Full higher order dependent type theory
11.6. Full higher order dependent type theory, categorically
11.7. Completeness of the category of PERs in the effective topos

Book

jacobs1999-categorical-logic.pdf

Octocurious

Explorer