Nifty. That was a nice 4-page exposé of the correspondence. There are no general proofs, but the correspondence between notations is very suggestive and invokes

Nifty. That was a nice 4-page exposé of the correspondence. There are no general proofs, but the correspondence between notations is very suggestive and invokes interesting intuitions, I think. The example derivations with the uncurry example are quite fun to work through. The paragraph about continuations corresponding to double negation is also super neat! Now I just wish there were something similar for the missing category theory third of the trinitary mentioned in another comment.