Diffractor comments on (A → B) → A

[Diffractor]

I found a paper about this exact sort of thing. Escardo and Olivia call that type signature a “selection functional”, and the type signature $(A\to B)\to B$ is called a “quantification functional”, and there’s several interesting things you can do with them, like combining multiple selection functionals into one in a way that looks reminiscent of game theory. (ie, if $ϵ$ has type signature $(A\to C)\to A$, and $\delta$ has type signature $(B\to C)\to B$, then $ϵ\otimes \delta$ has type signature $\left(\right(A\times B)\to C)\to (A\times B)$.