Church encoding of the booleans - a podcast by Aaron Stump

The Church encoding represents data as their own fold-right functions.  For booleans, this means they become their own if-then-else expressions.  We consider the polymorphic type for these, which is forall X. X -> X -> X.

Further episodes of Iowa Type Theory Commute

Further podcasts by Aaron Stump

Website of Aaron Stump