Conversation

Gödel’s dialectica interpretation looks like pattern-match deconstruction—counter-“witness” (aka way to deal with, accept as an argument) to \( A \vee B \) is *both* a way to deal with A and a way to deal with B (after inspecting tags)

https://link.springer.com/article/10.1007/BF02025118