Right, so. I’ve “known” for a while that sum types (enums) and product types (structs) are dual in a precise sense. I even kind of intuitively understood what that “precise sense” is. But this example was particularly visceral.

Here’s your bog-standard Church encoding of booleans:

For example, $if \: true \: 42 \: 101$ reduces to $42$, like you’d expect.

And here’s your Church encoding of pairs:

Wait, why do those inner lambdas in fst and snd look so familiar? And wait, isn’t pair just if with its arguments rearranged?

…Oh my god.