3 ms·
A good introduction to categorical logic is [0], introducing the simply-typed lambda calculus along with the categorical semantics for each construction (cartes
by siraben 6y ago
A good introduction to categorical logic is [0], introducing the simply-typed lambda calculus along with the categorical semantics for each construction (cartesian closed categories). The later sections include topics mentioned in this article such as hyperdoctrines, categorifying quantifiers, and dependent types.
[0] https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf https://www.cl.cam.ac.uk/~amp12/papers/catl/catl.pdf
- 3PS 6y agoCMU also currently has a course in categorical logic [0]. Internally, the only prerequisite is a course in category theory. The course notes can be found at [1]. [0] http://mathieu.anel.free.fr/CLcourse.html http://mathieu.anel.free.fr/CLcourse.html [1] http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlog(2019).pdf http://mathieu.anel.free.fr/mat/80514-814/Awodey-Bauer-catlo...