This book gives a survey of categorical logic and type theory starting from the unifying concept of a fibration. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists. To get an impression, the prospectus from the book is made available.

- By Peter Johnstone, in the
*Zentralblatt fur Mathematik*, vol. 905, 1999. - By Robert Seely,
*The Bulletin of Symbolic Logic*Vol. 6 (2000) No. 2, pp. 225-229 (available on the web). - By Andreas Blass, in
*Mathematical Reviews*2001b:03077.

2. The logic and type theory of sets

2. Some concrete examples: sets, omega-sets and PERs

3. Some general examples

4. Cloven and split fibrations

5. Change-of-base and composition of fibrations

6. Fibrations of signatures

7. Categories of fibrations

8. Fibrewise structure and fibred adjunctions

9. Products and coproducts

10. Indexed categories

2. Functorial semantics

3. Exponents, products and coproducts

4. Semantics of simple type theories

5. Semantics of the untyped lambda calculus as a corollary

6. Simple parameters

2. Specifications and theories in equational logic

3. Algebraic specifications

4. Fibred equality

5. Fibrations for equational logic

6. Fibred functorial semantics

2. Fibrations for first order predicate logic

4. Functorial interpretation and internal language

5. Subobject fibrations I: regular categories

6. Subobject fibrations II: coherent categories and logoses

7. Subset types

8. Quotient types

9. Quotient types, categorically

10. A logical characterisation of subobject fibrations

2. Generic objects

3. Fibrations for higher order logic

4. Elementary toposes

5. Colimits, powerobjects and well-poweredness in toposes

6. Nuclei in a topos

7. Separated objects and sheaves in a topos

8. A logical description of separated objects and sheaves

2. The effective topos and its subcategories of sets, omega-sets, and PERs

3. Families of PERs and omega-sets over the effective topos

4. Natural numbers in the effective topos and some associated principles

2. Internal functors and natural transformations

3. Externalisation

4. Internal diagrams and completeness

2. Use of polymorphic type theory

3. Naive set theoretic semantics

4. Fibrations for polymorphic type theory

5. Small polymorphic fibrations

6. Logic over polymorphic type theory

2. Logical predicates and relations

3. Quantification

4. Category theory over a fibration

5. Locally small fibrations

6. Definability

2. Use of dependent types

3. A term model

4. Display maps and comprehension categories

5. Closed comprehension categories

6. Domain theoretic models of type dependency

2. Dependent predicate logic, categorically

3. Polymorphic dependent type theory

4. Strong and very strong sum and equality

5. Full higher order dependent type theory

6. Full higher order dependent type theory, categorically

7. Completeness of the category of PERs in the effective topos

Last modified: Tue Oct 24 11:15:58 MEST 2006