Categorical Logic and Type Theory, Volume 141This 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
Prospectus | 1 |
Introduction to fibred category theory | 19 |
Simple type theory | 119 |
Equational Logic | 169 |
First order predicate logic | 219 |
Higher order predicate logic | 311 |
The effective topos | 373 |
Internal category theory | 407 |
Polymorphic type theory | 441 |
Advanced fibred category theory | 509 |
First order dependent type theory | 581 |
Higher order dependent type theory | 645 |
References | 717 |
| 735 | |
| 743 | |
Other editions - View all
Common terms and phrases
adjunction algebra Assume base category Beck-Chevalley Beck-Chevalley condition C₁ Cartesian closed Cartesian morphism Cartesian products change-of-base 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 natural numbers natural transformation obtained pair 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 split fibration strong structure Sub(B subobject fibration subset types terminal object Theorem topos total category type context UFam(PER UFam(w-Sets unique variables vertical w-Sets yields
Popular passages
Page 719 - A. Carboni, S. Lack, and RFC Walters. Introduction to extensive and distributive categories.
Page 719 - JRB Cockett and D. Spencer. Strong categorical datatypes I. In RAG Seely, editor, Category Theory 1991, number 13 in CMS Conference Proceedings, pages 141-169, 1992.
Page 725 - In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, volume 1 of Electronic Notes in Theoretical Computer Science, Tulane University, New Orleans, Louisiana, Mar.
Page 719 - About charity. Technical Report 92/480/18, Dep. Comp. Sci., Univ. Calgary, 1992. [5] JRB Cockett and D. Spencer. Strong categorical datatypes I. In RAG Seely, editor, Category Theory 1991, volume 13 of CMS Conference Proceedings, pages 141-169.