My motivation for this question is that I’m interested in using categorical logic/category theory to intuitively visualize and think about proofs in advanced type-theory based proof-assistants like Coq and Lean.

For that reason, I am interested in the following things:

  • proof by diagram chasing

  • the correspondence between types/propositions and objects in a category, and between proofs/programs and morphisms in that category. (I’m aware of the Curry-howard correspondence).

  • categorical logic in general.

Again, I’m primarily interested for the purpose of applying it in an intuitive way. Is there a good resource for this, given my motivation?


For book length works, I recommend the following:

  • Lambek & Scott's Introduction to Higher Order Categerical Logic. It has a nice brief introduction to category theory, and discusses typed lambda calculi and their relation to cartesian closed categories and a higher order type theory for toposes. It's a bit older, but still one of the best of its kind. It doesn't address dependent type theories of the sort Coq is based on, but it's a nice place to get started on thinking categorically about simple type theories.

  • A great book that covers a wide range of logics and type theories is Bart Jacobs' Categorical Logic and Type Theory. It's a little more demanding, and much longer, than Lambek & Scott, but it does give a very nice general account of type dependency, as well as spending a lot of time on realizability interpretations. The running theme of the book is the use of various forms of fibred category, a topic on which it is also one of the best resources I'm aware of.

The latter might be a bit overpowered for what you need, but reading the first chapter, skimming the examples of how fibrations are used to model logics, and getting the notion of a comprehension category would probably give you the main conceptual tools of the book.

If you need an additional category theory reference (the one in Lambek & Scott is adequate, but quick), a good and cheap one is Leinster's Basic Category Theory.

  • $\begingroup$ Thank you! Do you think that Lambek & Scott’s book is good for someone who just wants to apply it in practice, but doesn’t necessarily need all the deep theory? $\endgroup$ – user56834 Nov 11 '18 at 8:19
  • $\begingroup$ I think so, though I can't entirely promise that since I don't use it that way :P It does have some deep results, but a lot of it is also just establishing how cartesian closedness models currying, how natural number objects give you primitive recursion, that sort of thing. $\endgroup$ – Malice Vidrine Nov 11 '18 at 8:32
  • $\begingroup$ And if you wanted to keep your reading extra light when understanding type dependency, you could use what you learn from Lambek & Scott to tackle nLab articles like this one. You could probably piece together everything you'd need from Jacobs from nLab instead, with a bit of work. $\endgroup$ – Malice Vidrine Nov 11 '18 at 8:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.