Logical manifestations of topological concepts, and other things, via the univalent point of view.

Minimalistic dependent type theory with syntactic metaprogramming

Proofs for the exercises for Lawvere and Schanuel's Conceptual Mathematics

Using lambda calculus as the syntax for cartesian closed categories, ala Conal Elliott.

My Notes and Solutions from the CMU Hott Summer School