Categorical Logic and Type Theory
by Bart Jacobs · North Holland / Elsevier (Studies in Logic and the Foundations of Mathematics 141)
The reference volume once the correspondence in Lambek & Scott is understood: fibrations give one uniform machine for indexing logic over type contexts, which is what makes dependent and polymorphic type theory tractable categorically. Systematic survey organising the whole field around fibrations, covering simple, dependent, polymorphic and higher-order type theories alongside equational and first-order predicate logic. The author's page carries the full table of contents and a downloadable prospectus chapter.
This link may earn us a small commission at no extra cost to you. Affiliate disclosure
More resources on Categorical Logic
Wolfram MathWorld
MathWorld is an online mathematics encyclopedia from Wolfram Research offering detailed, browsable articles on topics across the math spectrum, including algebra, geometry, calculus, and number theory. Each entry includes definitions, theorems, formulas, diagrams, worked examples, and links to further reading.
nLab: Categorical Logic
nLab's reference entry on categorical logic, the study of logical systems through category theory: internal languages, hyperdoctrines, toposes, and the correspondence between type theories and structured categories. Useful for orientation and for its extensive links to related entries and literature.
Introduction to Higher-Order Categorical Logic
The primary source for the exact skill the topic promises: translating between formal proofs, programs and categorical structures. Establishes the correspondence between typed lambda calculi, intuitionistic proof theory and cartesian closed categories, then extends it to higher-order logic and toposes. The standard reference for the Curry-Howard-Lambek triangle linking proofs, programs and categorical structure.
Topoi: The Categorial Analysis of Logic
The least punishing rigorous route into how a category can carry a logic — it assumes far less than Mac Lane & Moerdijk or Johnstone and still reaches the real content (Heyting algebras of subobjects, quantifiers as adjoints, elementary toposes). Self-contained development of topos theory as a framework for logic, moving from arrows and categories through subobject algebras, intuitionistic versus classical semantics, adjoints as quantifiers, and categorial set theory. Roughly 550 pages, open access via Project Euclid.
Categorical Logic (CMU 80-514/814) — Course Notes
Steve Awodey's Carnegie Mellon graduate course page with downloadable chapter notes and problem sets covering functorial semantics of algebraic theories, propositional and first-order logic, simple and dependent type theory, topos theory, sheaf semantics, and homotopy type theory.
nLab
Collaborative wiki for mathematics, physics and philosophy written from a category-theoretic viewpoint, with cross-linked entries on categories, functors, adjunctions, topos theory, higher category theory and homotopy theory. Readers can look up precise definitions, examples and references for advanced structural mathematics.