UID:
almahu_9949697691102882
Format:
1 online resource (779 p.)
Edition:
1st ed.
ISBN:
1-281-04826-7
,
9786611048266
,
0-444-50853-8
,
0-08-052870-8
Series Statement:
Studies in logic and the foundations of mathematics ; v. 141
Content:
This 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.
Note:
Description based upon print version of record.
,
Cover; Preface; Contents; Preliminaries; Chapter 0. Prospectus; 0.1. Logic, type theory, and fibred category theory; 0.2. The logic and type theory of sets; Chapter 1. Introduction to fibred category theory; 1.1. Fibrations; 1.2. Some concrete examples: sets, ?-sets and PERs; 1.3. Some general examples; 1.4. Cloven and split fibrations; 1.5. Change-of-base and composition for fibrations; 1.6. Fibrations of signatures; 1.7. Categories of fibrations; 1.8. Fibrewise structure and fibred adjunctions; 1.9. Fibred products and coproducts; 1.10. Indexed categories; Chapter 2. Simple type theory
,
2.1. The basic calculus of types and terms2.2. Functorial semantics; 2.3. Exponents, products and coproducts; 2.4. Semantics of simple type theories; 2.5. Semantics of the untyped lambda calculus as a corollary; 2.6. Simple parameters; Chapter 3. Equational Logic; 3.1. Logics; 3.2. Specifications and theories in equational logic; 3.3. Algebraic specifications; 3.4. Fibred equality; 3.5. Fibrations for equational logic; 3.6. Fibred functorial semantics; Chapter 4. First order predicate logic; 4.1. Signatures, connectives and quantifiers; 4.2. Fibrations for first order predicate logic
,
4.3. Functorial interpretation and internal language4.4. Subobject fibrations I: regular categories; 4.5. Subobject fibrations II: coherent categories and logoses; 4.6. Subset types; 4.7. Quotient types; 4.8. Quotient types, categorically; 4.9. A logical characterisation of subobject fibrations; Chapter 5. Higher order predicate logic; 5.1. Higher order signatures; 5.2. Generic objects; 5.3. Fibrations for higher order logic; 5.4. Elementary toposes; 5.5. Colimits, powerobjects and well-poweredness in a topos; 5.6. Nuclei in a topos; 5.7. Separated objects and sheaves in a topos
,
5.8. A logical description of separated objects and sheavesChapter 6. The effective topos; 6.1. Constructing a topos from a higher order fibration; 6.2. The effective topos and its subcategories of sets, ?-sets, and PERs; 6.3. Families of PERs and ?-sets over the effective topos; 6.4. Natural numbers in the effective topos and some associated principles; Chapter 7. Internal category theory; 7.1. Definition and examples of internal categories; 7.2. Internal functors and natural transformations; 7.3. Externalisation; 7.4. Internal diagrams and completeness; Chapter 8. Polymorphic type theory
,
8.1. Syntax8.2. Use of polymorphic type theory; 8.3. Naive set theoretic semantics; 8.4. Fibrations for polymorphic type theory; 8.5. Small polymorphic fibrations; 8.6. Logic over polymorphic type theory; Chapter 9. Advanced fibred category theory; 9.1. Opfibrations and fibred spans; 9.2. Logical predicates and relations; 9.3. Quantification; 9.4. Category theory over a fibration; 9.5. Locally small fibrations; 9.6. Definability; Chapter 10. First order dependent type theory; 10.1. A calculus of dependent types; 10.2. Use of dependent types; 10.3. A term model
,
10.4. Display maps and comprehension categories
,
English
Additional Edition:
ISBN 0-444-50170-3
Language:
English
