## Categorical Logic and Type TheoryThis 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. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### 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 |

Advanced fibred category theory | 509 |

First order dependent type theory | 581 |

Higher order dependent type theory | 645 |

735 | |

743 | |

### Other editions - View all

### Common terms and phrases

adjunction algebra arbitrary Assume base category Beck-Chevalley Beck-Chevalley condition canonical map Cartesian closed Cartesian morphism Cartesian products category IB category theory change-of-base codomain fibration commuting comonad composition comprehension category Consider construction coproducts correspondence Dcpo define Definition dependent type theory described diagram display map effective topos Eq-fibration equaliser equations example Exercise exponents Fam(C fibred categories fibred functor finite limits Frobenius full and faithful function symbols Hence higher order logic indexed category internal category isomorphism kinds left adjoint Lemma mono natural numbers natural transformation obtained pair polymorphic type theory poset predicate logic preorder preserves products and coproducts projection Proof Prop Proposition pullback pullback square quantification quotient types result right adjoint satisfying Sets Show signature simple fibration simple type theory slice category split fibration structure subobject fibration subset types terminal object Theorem topos total category type context UFam(PER unique 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.