category theory meets logic

[larrytheliquid]

Here's an in-progress set of notes on an "Introduction to Categorical
Logic". Pretty awesome as it goes into Heyting algebras,
intuitionistic logic, curry-howard isomorphism, and even dependent
types!

http://www.andrew.cmu.edu/user/awodey/catlog/notes/