The Computational Trilogy: Three Languages for One Structure

A guy tries to explain why proofs, programs, and morphisms keep turning into each other.