The Yoda embedding, contravariant it is.
CPS Transform for CBV STLC
Took the translation from here, which is probably the most concise way to write it:
\[\newcommand{cps}[1]{[\![#1]\!]} \newcommand{app}[2]{\left(#1\ #2\right)} \newcommand{\block}[1]{\left(#1\right)} \newcommand{if}[3]{\block{\text{if}\ #1\ #2\ #3}} \begin{align} \cps{x} &= \lambda \kappa.\app{\kappa}{x} \\ \cps{\lambda x.e} &= \lambda \kappa.\app{\kappa}{\lambda x.\cps{e}} \\ \cps{\app{f}{e}} &= \lambda \kappa.\app{\cps{f}}{\lambda f.\app{\cps{e}}{\lambda e.\block{f\ e\ \kappa}}} \\ \end{align}\]From a type perspective, say x :B, then $\cps{x}$ : $(B \rightarrow C) \rightarrow C$. Similarly, say f : $A \rightarrow B$ and e : A, then $ \cps{\app{f}{e}} $: $(B \rightarrow C) \rightarrow C$. In the second line, say x : A, e: B, then $\kappa$ : $A \rightarrow (B \rightarrow C)) \rightarrow C$, which is the same type as the $f$ continuation. And $\cps{\lambda x.e}$ : $(A \rightarrow (B \rightarrow C)) \rightarrow C) \rightarrow C$
Yoneda Embedding?
max new貌似写过一个相关的blog post
Sidenode: The origin of the name Yoneda Embedding
Glivenko’s theorem
The proof of this also resembles the flavor of CPS.