Categorical Logic and Type 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.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
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