Iowa Type Theory Commute
The basic idea of the Curry-Howard isomorphism, and its connection to the contents of Chapters 1 and 2. Constructive proof. A famous nonconstructive proof.