# reperiendi

## Yoneda embedding as contrapositive and call-cc as double negation

Posted in Category theory, Math, Programming by Mike Stay on 2008 January 26

Consider the problem of how to represent negation of a proposition $P$ when we only have implication and falsehood:

$P \to {\rm F}.$

Since ${\rm F} \to {\rm F}$ is true and ${\rm T} \to {\rm F}$ is false, this does what we want.

The contrapositive says $\neg Q \to \neg P$ has the same truth value as $P \to Q.$ Using only implication, the contrapositive of $P \to Q$ is

$(Q \to {\rm F}) \to (P \to {\rm F}).$

What if we don’t even have falsehood? Well, we can pick any proposition $X$ to represent falsehood and form

$(Q \to X) \to (P \to X).$

The Yoneda embedding takes a category $C^{\rm op}$ and produces a category $\mbox{HOM}(C, \mbox{Set})$:

$\begin{array}{ccccccc}\mbox{Yoneda}_X: & C^{\rm op} & \to & \mbox{HOM}(C, \mbox{Set}) \\ & P & \mapsto & \mbox{hom}(P, X) \\ & f:P \to Q & \mapsto & \mbox{Yoneda}_X(f): & \mbox{hom}(Q, X) & \to & \mbox{hom}(P, X) \\ & & & & k & \mapsto & k \circ f \end{array}$

This embedding is better known among computer scientists as the continuation passing style transformation.

In a symmetric monoidal closed category, like lambda calculus, we can move everything “inside:” every morphism $f:P \to Q$ has an internal version $f:I\to P \multimap Q.$ The internal Yoneda embedding of $f$ is

$\mbox{Yoneda}_X(f):I \to (Q \multimap X) \multimap (P \multimap X).$

Here $I$ is the “unit” type; notice how the target type is isomorphic under the Curry-Howard isomorphism to the contrapositive. This is a term that maps a continuation $k:Q\multimap X$ and a value $p:P$ to $k(f(p)).$

To get double negation, first do the Yoneda embedding on the identity to get

$\mbox{Yoneda}_X(1_P):hom(P,X) \to hom(P,X),$

then uncurry, braid, and recurry to get

$\mbox{Yoneda}_X(1_P):P \to hom(hom(P,X),X),$

or, internally,

$\mbox{Yoneda}_X(1_P):I\to P \multimap ((P\multimap X)\multimap X).$

This takes a value $p$ to a function value $k\mapsto k(p).$

Call-with-current-continuation expects a term that has been converted to CPS style as above, and then hands it the remainder of the computation in $k.$