Is there some sort of function transformation expressing $(X\implies Y)\Leftrightarrow (\neg X\lor Y)$? Is there a functional interpretation if the replacement for for the material implication?:
$$(X\implies Y)\Leftrightarrow (\neg X\lor Y)$$
Given a function from type $X$ to type $Y$, viewed as a witness of the proposition $X\implies Y$, can I obtain a proof for $\neg X\lor Y$? The connective "$\lor$" gets translated to a pair - I fail to see how this relates to a function/process, something which doesn't even require a proof of $X$.

It took me a while to find the post, but Neighborhood of Infinity's Exceptions, Disjunctions, and Continuations describes this topic. I haven't fully understood everything presented there, but the author asks about the isomorhism between $a \to b$ and $\lnot a \lor b$, what the type $\lnot a$ means ($a \to \bot$), and what $\lnot\lnot a$ means ($(a \to \bot) \to \bot$), and so on.  I'm not sure whether it will answer your question or not, but it might prove a useful starting point for you, or some other answer-ers.
