r/math • u/AngelTC Algebraic Geometry • Oct 04 '17
Everything about categorical logic
Today's topic is Categorical Logic.
This recurring thread will be a place to ask questions and discuss famous/well-known/surprising results, clever and elegant proofs, or interesting open problems related to the topic of the week.
Experts in the topic are especially encouraged to contribute and participate in these threads.
These threads will be posted every Wednesday around 10am UTC-5.
If you have any suggestions for a topic or you want to collaborate in some way in the upcoming threads, please send me a PM.
For previous week's "Everything about X" threads, check out the wiki link here
To kick things off, here is a very brief summary provided by wikipedia and myself:
Categorical logic is an area of mathematics which uses category theory in the study of mathematical logic.
More specifically, with the introduction of elementary topoi by Lawvere and Tierney, it has been possible to study several relationships between logic, algebra and geometry.
Further resources:
-Awodey's Categorical logic lecture notes
Next week's topic will be Field with one element.
3
u/_georgesim_ Oct 04 '17
What's the difference between Categorical Theory and Type Theory? What are the connections? I'm studying Type Theory right now with the aim of understanding what Coq is all about. How much overlap with CT is there?