How to simulate booleans in simply typed lambda calculus?

I have been writing lecture notes on computable mathematics. One of the questions that came up was whether it is possible to simulate the booleans in the simply-typed λ-calculus. This is a nice puzzle in functional programming. If you solve it, definitely let me know, although I suspect logicians did it a long time ago. Continue reading How to simulate booleans in simply typed lambda calculus?