Re: On on

On Thu, Nov 02, 2006 at 05:35:22PM +0100, Nils Anders Danielsson wrote:

And now Ulf is in the process of proving that flip on is a functor from C to C^op for any CCC C, with flip on defined as follows:

flip_on_A(B) = (A^B)^B flip_on_A(f) = curry (curry (eval ??? id × f) ??? eval ??? id × f)

It's the continuation-passing version of (^2) : C -> C.