Introduction to categorical logic and CHL-correspondence?

Question

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?

Answer 1

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.