Categorical Logic and Type Theory (eBook)

Cover 1
Preface 6
Contents 8
Preliminaries 12
Chapter 0. Prospectus 20
0.1. Logic, type theory, and fibred category theory 20
0.2. The logic and type theory of sets 30
Chapter 1. Introduction to fibred category theory 38
1.1. Fibrations 39
1.2. Some concrete examples: sets, .-sets and PERs 50
1.3. Some general examples 59
1.4. Cloven and split fibrations 66
1.5. Change-of-base and composition for fibrations 75
1.6. Fibrations of signatures 83
1.7. Categories of fibrations 91
1.8. Fibrewise structure and fibred adjunctions 99
1.9. Fibred products and coproducts 112
1.10. Indexed categories 126
Chapter 2. Simple type theory 138
2.1. The basic calculus of types and terms 139
2.2. Functorial semantics 145
2.3. Exponents, products and coproducts 152
2.4. Semantics of simple type theories 165
2.5. Semantics of the untyped lambda calculus as a corollary 173
2.6. Simple parameters 176
Chapter 3. Equational Logic 188
3.1. Logics 189
3.2. Specifications and theories in equational logic 196
3.3. Algebraic specifications 202
3.4. Fibred equality 209
3.5. Fibrations for equational logic 220
3.6. Fibred functorial semantics 228
Chapter 4. First order predicate logic 238
4.1. Signatures, connectives and quantifiers 240
4.2. Fibrations for first order predicate logic 251
4.3. Functorial interpretation and internal language 265
4.4. Subobject fibrations I: regular categories 275
4.5. Subobject fibrations II: coherent categories and logoses 284
4.6. Subset types 291
4.7. Quotient types 301
4.8. Quotient types, categorically 309
4.9. A logical characterisation of subobject fibrations 323
Chapter 5. Higher order predicate logic 330
5.1. Higher order signatures 331
5.2. Generic objects 340
5.3. Fibrations for higher order logic 349
5.4. Elementary toposes 357
5.5. Colimits, powerobjects and well-poweredness in a topos 365
5.6. Nuclei in a topos 372
5.7. Separated objects and sheaves in a topos 379
5.8. A logical description of separated objects and sheaves 387
Chapter 6. The effective topos 392
6.1. Constructing a topos from a higher order fibration 393
6.2. The effective topos and its subcategories of sets, .-sets, and PERs 404
6.3. Families of PERs and .-sets over the effective topos 412
6.4. Natural numbers in the effective topos and some associated principles 417
Chapter 7. Internal category theory 426
7.1. Definition and examples of internal categories 427
7.2. Internal functors and natural transformations 433
7.3. Externalisation 440
7.4. Internal diagrams and completeness 449
Chapter 8. Polymorphic type theory 460
8.1. Syntax 463
8.2. Use of polymorphic type theory 473
8.3. Naive set theoretic semantics 482
8.4. Fibrations for polymorphic type theory 490
8.5. Small polymorphic fibrations 504
8.6. Logic over polymorphic type theory 514
Chapter 9. Advanced fibred category theory 528
9.1. Opfibrations and fibred spans 529
9.2. Logical predicates and relations 537
9.3. Quantification 554
9.4. Category theory over a fibration 566
9.5. Locally small fibrations 577
9.6. Definability 587
Chapter 10. First order dependent type theory 600
10.1. A calculus of dependent types 603
10.2. Use of dependent types 613
10.3. A term model 620
10.4. Display maps and comprehension categories 628
10.5. Closed comprehension categories 642
10.6. Domain theoretic models of type dependency 656
Chapter 11. Higher order dependent type theory 664
11.1. Dependent predicate logic 667
11.2. Dependent predicate logic, categorically 672
11.3. Polymorphic dependent type theory 681
11.4. Strong and very strong sum and equality 693
11.5. Full higher order dependent type theory 703
11.6. Full higher order dependent type theory, categorically 711
11.7. Completeness of the category of PERs in the effective topos 726
References 736
Notation Index 754
Subject Index 762