Categorical Logic and Type TheoryThis book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists. |
Contents
| 1 | |
| 19 | |
Chapter 2 Simple type theory | 119 |
Chapter 3 Equational Logic | 169 |
Chapter 4 First order predicate logic | 219 |
Chapter 5 Higher order predicate logic | 311 |
Chapter 6 The effective topos | 373 |
Chapter 7 Internal category theory | 407 |
Chapter 8 Polymorphic type theory | 441 |
Chapter 9 Advanced fibred category theory | 509 |
Chapter 10 First order dependent type theory | 581 |
Chapter 11 Higher order dependent type theory | 645 |
| 717 | |
| 735 | |
| 743 | |
Other editions - View all
Common terms and phrases
adjunction algebra Assume base category Beck-Chevalley Beck-Chevalley condition Cartesian closed Cartesian morphism Cartesian products category theory change-of-base Cº(XX codomain fibration commuting comonad comprehension category Consider construction coproducts correspondence define Definition dependent type theory described diagram effective topos Eq-fibration equaliser equality equations equivalence example Exercise exponents Fam(C family fibration fibred categories fibred functor finite limits Frobenius full and faithful function symbols indexed category internal category isomorphism kinds left adjoint Lemma mono morphism f natural numbers natural transformation polymorphic type theory predicate logic preorder preserves products and coproducts projection Proof Prop Proposition pullback quantification quotient types relation result right adjoint Sets Show signature simple fibration simple type theory slice category split fibration strong structure subobject fibration subset types T H M terminal object Theorem topos total category type context UFam(PER unique variables vertical w-Sets w–Sets yields