You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Nathaniel Virgo (Sep 23 2023 at 01:13):I'd like to understand the relationship between the simply typed lambda calculus and Cartesian closed categories. (I have heard that simply typed lambda calculus is the internal language of a Cartesian closed category, but I don't know what that means.) I know this is part of a much bigger family of concepts involving toposes, fibrations and dependent type theory, but I'm hoping I can start small and work up. So I'm hoping to see the connection between lambda calculus and closed Cartesian categories clearly without going on too much of an excursion through those other topics first. Is there an easy way to see it, or a resource that explains it?
My background is such that I know my way around Cartesian closed categories pretty well and simply typed lambda calculus reasonably well, but I don't have any clear idea of what an internal language is or how it relates to an [[internal logic]]. I don't have much background in logic, and specifically I don't have any prior knowledge of how lambda calculi and logic are related.
Evan Patterson (Sep 23 2023 at 01:23):Roy Crole's book Categories for Types explains the relationship between algebraic theories and cartesian categories, and between simply typed lambda calculus and cartesian closed categories, in a lot of detail. IMO, it's a nice place to start if you want to learn some of the main ideas of categorical logic: functorial semantics, internal languages, and classifying categories.
Damiano Mazza (Sep 23 2023 at 08:09):If you want to have the "full picture", Part D of the Elephant (vol. 2) covers categorical logic quite thoroughly. In particular, the first chapter (D1) introduces the concepts of internal language and syntactic category in full detail. That chapter deals only with first-order theories, the -calculus is covered much later in the book (section D4.2, and you don't really need to read everything in between), but I think that once you know how that works, the higher-order case is an expected generalization, and it's not necessarily easier conceptually. Probably the Elephant is not the best source to use as a first introduction, but for this particular topic I think it's ok (personally, that's how I first learned categorical logic).
Damiano Mazza (Sep 23 2023 at 08:13):Otherwise, if you want to go straight to your question without going through first-order categorical logic, the standard reference is Lambek and Scott's Introduction to higher order categorical logic. It's available online (just google something like "lambek scott categorical logic"). I never read it but Part I is called "Cartesian closed categories and the -calculus". Sounds promising :big_smile:
John Baez (Sep 23 2023 at 09:25):You might try my course notes on the lambda calculus and closed categories:
I was learning this material from Lambek and Scott's book, conversations with @Mike Stay and other sources (listed on these web pages).
John Baez (Sep 23 2023 at 09:26):In these course notes I talk about:
John Baez (Sep 23 2023 at 09:29):We further developed some — but far from all! — of the material in my course notes in this long paper:
Nathaniel Virgo (Sep 23 2023 at 11:46):That sounds great! I was reading some of that paper earlier today, having realised it might be relevant. I'll check out the other resources as well.
Mike Shulman (Sep 23 2023 at 15:08):My unfinished categorical logic notes start from even simpler type theories and their corresponding categories, and build up to STLCs/CCCs and then on to first-order logic.
Kevin Arlin (Sep 23 2023 at 18:49):I assume there's no particular prospect of you finding time to work on those notes further is there, Mike? I like them a lot.
Mike Shulman (Sep 23 2023 at 19:11):Not in the near future, unfortunately, but I definitely intend to finish them one day.
Eduardo Ochs (Sep 24 2023 at 22:53):I published some papers on "Categories for Children", and they practically start with CCCs and the simply-typed λ-calculus... take a look a the introduction of the first link below and at the section 5.5 ("A way to teach adjuctions") in the second link:
http://anggtwu.net/LATEX/2017planar-has-1.pdf
http://anggtwu.net/LATEX/2022on-the-missing.pdf#page=26