| Preface |
|
v | |
| Contents |
|
vii | |
| Preliminaries |
|
xi | |
|
|
|
1 | (18) |
|
Logic, type theory, and fibred category theory |
|
|
1 | (10) |
|
The logic and type theory of sets |
|
|
11 | (8) |
|
Introduction to fibred category theory |
|
|
19 | (100) |
|
|
|
20 | (11) |
|
Some concrete examples: sets, σ-sets and PERs |
|
|
31 | (9) |
|
|
|
40 | (7) |
|
Cloven and split fibrations |
|
|
47 | (9) |
|
Change-of-base and composition for fibrations |
|
|
56 | (8) |
|
|
|
64 | (8) |
|
|
|
72 | (8) |
|
Fibrewise structure and fibred adjunctions |
|
|
80 | (13) |
|
Fibred products and coproducts |
|
|
93 | (14) |
|
|
|
107 | (12) |
|
|
|
119 | (50) |
|
The basic calculus of types and terms |
|
|
120 | (6) |
|
|
|
126 | (7) |
|
Exponents, products and coproducts |
|
|
133 | (13) |
|
Semantics of simple type theories |
|
|
146 | (8) |
|
Semantics of the untyped lambda calculus as a corollary |
|
|
154 | (3) |
|
|
|
157 | (12) |
|
|
|
169 | (41) |
|
|
|
170 | (7) |
|
Specifications and theories in equational logic |
|
|
177 | (6) |
|
|
|
183 | (7) |
|
|
|
190 | (11) |
|
Fibrations for equational logic |
|
|
201 | (1) |
|
Fibred functorial semantics |
|
|
201 | (9) |
|
First order predicate logic |
|
|
210 | (101) |
|
Signatures, connectives and quantifiers |
|
|
221 | (11) |
|
Fibrations for first order predicate logic |
|
|
232 | (14) |
|
Functorial interpretation and internal language |
|
|
246 | (10) |
|
Subobject fibrations I: regular categories |
|
|
256 | (9) |
|
Subobject fibrations II: coherent categories and logoses |
|
|
265 | (7) |
|
|
|
272 | (10) |
|
|
|
282 | (8) |
|
Quotient types, categorically |
|
|
290 | (14) |
|
A logical characterisation of subobject fibrations |
|
|
304 | (7) |
|
Higher order predicate logic |
|
|
311 | (62) |
|
|
|
312 | (9) |
|
|
|
321 | (9) |
|
Fibrations for higher order logic |
|
|
330 | (8) |
|
|
|
338 | (8) |
|
Colimits, powerobjects and well-poweredness in a topos |
|
|
346 | (7) |
|
|
|
353 | (7) |
|
Separated objects and sheaves in a topos |
|
|
360 | (8) |
|
A logical description of separated objects and sheaves |
|
|
368 | (5) |
|
|
|
373 | (34) |
|
Constructing a topos from a higher order fibration |
|
|
374 | (11) |
|
The effective topos and its subcategories of sets, σ-sets, and PERs |
|
|
385 | (8) |
|
Families of PERs and w-sets over the effective topos |
|
|
393 | (5) |
|
Natural numbers in the effective topos and some associated principles |
|
|
398 | (9) |
|
|
|
407 | (34) |
|
Definition and examples of internal categories |
|
|
408 | (6) |
|
Internal functors and natural transformations |
|
|
414 | (7) |
|
|
|
421 | (9) |
|
Internal diagrams and completeness |
|
|
430 | (11) |
|
|
|
441 | (68) |
|
|
|
444 | (10) |
|
Use of Polymorphic type theory |
|
|
454 | (9) |
|
Naive set theoretic semantics |
|
|
463 | (8) |
|
Fibrations for polymorphic type theory |
|
|
471 | (14) |
|
Small polymorphic fibrations |
|
|
485 | (10) |
|
Logic over polymorphic type theory |
|
|
495 | (14) |
|
Advanced fibred category theory |
|
|
509 | (72) |
|
Opfibrations and fibred spans |
|
|
510 | (8) |
|
Logical predicates and relations |
|
|
518 | (17) |
|
|
|
535 | (12) |
|
Category theory over a fibration |
|
|
547 | (11) |
|
|
|
558 | (10) |
|
|
|
568 | (13) |
|
First order dependent type theory |
|
|
581 | (64) |
|
A calculus of dependent types |
|
|
584 | (10) |
|
|
|
594 | (7) |
|
|
|
601 | (8) |
|
Display maps and comprehension categories |
|
|
609 | (14) |
|
Closed comprehension categories |
|
|
623 | (14) |
|
Domain theoretic models of type dependency |
|
|
637 | (8) |
|
Higher order dependent type theory |
|
|
645 | (72) |
|
Dependent predicate logic |
|
|
648 | (5) |
|
Dependent predicate logic, categorically |
|
|
653 | (9) |
|
Polymorphic dependent type theory |
|
|
662 | (12) |
|
Strong and very strong sum and equality |
|
|
674 | (15) |
|
Full higher order dependent type theory |
|
|
689 | (3) |
|
Full higher order dependent type theory, categorically |
|
|
692 | (15) |
|
Completeness of the category of PERs in the effective topos |
|
|
707 | (10) |
| References |
|
717 | (18) |
| Notation Index |
|
735 | (8) |
| Subject Index |
|
743 | |
