LIMITED OFFER

## Save 50% on book bundles

Immediately download your ebook while waiting for your print delivery. No promo code is needed.

Skip to main content# Categorical Logic and Type Theory

## Purchase options

## Save 50% on book bundles

## Institutional subscription on ScienceDirect

Request a sales quote**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.** Definition and examples of internal categories. Internal functors and natural transformations. Externalisation. Internal diagrams and completeness. **Polymorphic type theory.** Syntax. Use of polymorphic type theory. Naive set theoretic semantics. Fibrations for polymorphic type theory. Small polymorphic fibrations. Logic over polymorphic type theory. **Advanced fibred category theory.** Opfibrations and fibred spans. Logical predicates and relations. Quantification. Category theory over a fibration. Locally small fibrations. Definability. **First order dependent type theory.** A calculus of dependent types. Use of dependent types. A term model. Display maps and comprehension categories. Closed comprehension categories. Domain theoretic models of type dependency. **Higher order dependent type theory.** Dependent predicate logic. Dependent predicate logic, categorically. Polymorphic dependent type theory. Strong and very strong sum and equality. Full higher order dependent type theory. Full higher order dependent type theory, categorically. Completeness of the category of PERs in the effective topos. **References. Notation index. Subject index.**### B. Jacobs

Save up to 30% on Elsevier print and eBooks with free shipping. No promo code needed.

Save up to 30% on print and eBooks.

1st Edition, Volume 141 - January 14, 1999

Author: B. Jacobs

Language: EnglishPaperback ISBN:

9 7 8 - 0 - 4 4 4 - 5 0 8 5 3 - 9

eBook ISBN:

9 7 8 - 0 - 0 8 - 0 5 2 8 7 0 - 0

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… Read more

LIMITED OFFER

Immediately download your ebook while waiting for your print delivery. No promo code is needed.

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: 778
- Language: English
- Edition: 1
- Volume: 141
- Published: January 14, 1999
- Imprint: Elsevier Science
- Paperback ISBN: 9780444508539
- eBook ISBN: 9780080528700

BJ

Affiliations and expertise

Computing Science Institute, University of Nijmegen, The NetherlandsRead *Categorical Logic and Type Theory* on ScienceDirect