Categorical Logic and Type Theory - 1st Edition - ISBN: 9780444501707, 9780080929781

Categorical Logic and Type Theory, Volume 141

1st Edition

Authors: B. Jacobs
eBook ISBN: 9780080929781
eBook ISBN: 9780080528700
Paperback ISBN: 9780444508539
Imprint: Elsevier Science
Published Date: 14th January 1999
Page Count: 778
Sales tax will be calculated at check-out Price includes VAT/GST
Price includes VAT/GST
× Read this ebook on your PC, Mac, Apple iOS and Andriod mobile devices and eReader

This ebook is protected by Adobe Content Server digital rights management.

For more information on how to use .acsm files please click the Ebook Format Help link.

Institutional Access

Secure Checkout

Personal information is secured with SSL technology.

Free Shipping

Free global shipping
No minimum order.

Table of Contents

Preface. Contents. Preliminaries. Prospectus. Logic, type theory, and fibred category theory. The logic and type theory of sets. Introduction to fibred category theory. Fibrations. Some concrete examples: sets, &ohgr;-sets and PERs. Some general examples. Cloven and split fibrations. Change-of-base and composition for fibrations. Fibrations of signatures. Categories of fibrations. Fibrewise structure and fibred adjunctions. Fibred products and coproducts. Indexed categories. Simple type theory. The basic calculus of types and terms. Functorial semantics. Exponents, products and coproducts. Semantics of simple type theories. Semantics of the untyped lambda calculus as a corollary. Simple parameters. Equational logic. Logics. Specifications and theories in equational logic. Algebraic specifications. Fibred equality. Fibrations for equational logic. Fibred functorial semantics. First order predicate logic. Signatures, connectives and quantifiers. Fibrations for the first order predicate logic. Functorial interpretation and internal language. Subobject fibrations I: regular categories. Subobject fibrations II: coherent categories and logoses. Subset types. Quotient types. Quotient types, categorically. A logical characterisation of subobject fibrations. Higher order predicate logic. Higher order signatures. Generic objects. Fibrations for higher order logic. Elementary toposes. Colimits, powerobjects and well-poweredness in topos. Nuclei in a topos. Separated objects and sheaves in a topos. A logical description of separated objects and sheaves. The effective topos. Constructing a topos from a higher order fibration. The effective topos and its subcategories of sets, &ohgr;-sets, and PERs. Families of PERs, and &ohgr;-sets over the effective topos. Natural numbers in the effective topos and some associated principles. Internal category theory.</


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.


No. of pages:
© Elsevier Science 1998
Elsevier Science
eBook ISBN:
eBook ISBN:
Paperback ISBN:


@qu:...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... @source:Zentralblatt für Mathematik, vol.905 @from:R.A.G. Seely @qu:This book will be the standard reference in its field for some time to come. @source:The Bulletin of Symbolic Logic, Vol. 6

Ratings and Reviews

About the Authors

B. Jacobs Author

Affiliations and Expertise

Computing Science Institute, University of Nijmegen, The Netherlands