# Introduction to categorical logic and CHL-correspondence?

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.

• 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? – user56834 Nov 11 '18 at 8:19
• 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. – Malice Vidrine Nov 11 '18 at 8:32
• 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. – Malice Vidrine Nov 11 '18 at 8:37