Atjaunināt sīkdatņu piekrišanu

Categorical Logic and Type Theory, Volume 141 [Hardback]

(Computing Science Institute, University of Nijmegen, The Netherlands)
Citas grāmatas par šo tēmu:
Categorical Logic and Type Theory, Volume 141Palielināt
Citas grāmatas par šo tēmu:
Permanent link: https://www.kriso.lv/db/9780444501707.html
Keywords:
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.

Recenzijas

"The author's achievement in collecting and organizing a very large body of material in coherent form,... this is first and foremost an encyclopaedic work, into which specialists will delve with much pleasure and profit... One very welcome feature of the book is a comprehensive bibliography of nearly 350 items..." --Zentralblatt für Mathematik, vol.905R.A.G. Seely"This book will be the standard reference in its field for some time to come." --The Bulletin of Symbolic Logic, Vol. 6

Preface v
Contents vii
Preliminaries xi
Prospectus
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)
Fibrations
20(11)
Some concrete examples: sets, ω-sets and PERs
31(9)
Some general examples
40(7)
Cloven and split fibrations
47(9)
Change-of-base and composition for fibrations
56(8)
Fibrations of signatures
64(8)
Categories of fibrations
72(8)
Fibrewise structure and fibred adjunctions
80(13)
Fibred products and coproducts
93(14)
Indexed categories
107(12)
Simple type theory
119(50)
The basic calculus of types and terms
120(6)
Functorial semantics
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)
Simple parameters
157(12)
Equational Logic
169(50)
Logics
170(7)
Specifications and theories in equational logic
177(6)
Algebraic specifications
183(7)
Fibred equality
190(11)
Fibrations for equational logic
201(8)
Fibred functorial semantics
209(10)
First order predicate logic
219(92)
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)
Subset types
272(10)
Quotient types
282(8)
Quotient types, categorically
290(14)
A logical characterisation of subobject fibrations
304(7)
Higher order predicate logic
311(62)
Higher order signatures
312(9)
Generic objects
321(9)
Fibrations for higher order logic
330(8)
Elementary toposes
338(8)
Colimits, powerobjects and well-poweredness in a topos
346(7)
Nuclei in a topos
353(7)
Separated objects and sheaves in a topos
360(8)
A logical description of separated objects and sheaves
368(5)
The effective topos
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 ω-sets over the effective topos
393(5)
Natural numbers in the effective topos and some associated principles
398(9)
Internal category theory
407(34)
Definition and examples of internal categories
408(6)
Internal functors and natural transformations
414(7)
Externalisation
421(9)
Internal diagrams and completeness
430(11)
Polymorphic type theory
441(68)
Syntax
444(10)
Use of polymorphic type theory
454(9)
Native 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)
Quantification
535(12)
Category theory over a fibration
547(11)
Locally small fibrations
558(10)
Definability
568(13)
First order dependent type theory
581(64)
A calculus of dependent types
584(10)
Use of dependent types
594(7)
A term model
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(10)
Full higher order dependent type theory
684(8)
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