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

1 | |

19 | |

Chapter 2 Simple type theory | 119 |

Chapter 3 Equational Logic | 169 |

Chapter 4 First order predicate logic | 219 |

Chapter 5 Higher order predicate logic | 311 |

Chapter 6 The effective topos | 373 |

Chapter 7 Internal category theory | 407 |

Chapter 8 Polymorphic type theory | 441 |

Chapter 9 Advanced fibred category theory | 509 |

Chapter 10 First order dependent type theory | 581 |

Chapter 11 Higher order dependent type theory | 645 |

717 | |

735 | |

743 | |

### Other editions - View all

### Common terms and phrases

adjunction algebra Assume base category Beck-Chevalley Beck-Chevalley condition calculus Cartesian closed Cartesian closed category Cartesian morphism Cartesian products category theory change-of-base codomain ﬁbration commuting comonad comprehension category Consider construction coproducts correspondence Dcpo deﬁnable deﬁne Deﬁnition dependent type theory described diagram display map effective topos Eq-ﬁbration equaliser equality equations equivalence example Exercise exponents Fam(C family ﬁbration ﬁbre ﬁbred categories ﬁbred functor ﬁnite limits ﬁrst order Frobenius full and faithful function symbols indexed category internal category isomorphism kinds left adjoint Lemma mono natural numbers natural transformation pair polymorphic type theory predicate logic preorder preserves products and coproducts projection Proof Prop Proposition pullback quantiﬁcation quotient types relation result right adjoint satisﬁes Sets Show signature simple ﬁbration simple type theory slice category speciﬁcation split ﬁbration strong structure subobject ﬁbration subset types terminal object Theorem topos total category type context UFam(PER unique vertical w-Sets yields