This episode is about Chapter 2 of the Agda book.  Agda is based on the Curry-Howard isomorphism, which identifies typed (pure) functional programs and constructive proofs.  In this episode, I introduce the idea of the Curry-Howard isomorphism, and constructive versus classical reasoning.