rewrite_plus.scala

// a very basic Scala function performing a simple operation on primitive type Int
def plus = (x:Int) => (y:Int) => x + y

// First, we need to reify our CCC world
val K = implicitly[CartesianClosedCat[Function1]]
// now we import CCC language into our context
import K._

// pseudo-code
// we can always uncurry curried function
uncurry((x:Int) => (y:Int) => x + y) ≌ (x:Int, y:Int) => x + y
// remind projections
(x:Int, y:Int) => x ≌ exl[Int, Int]
(x:Int, y:Int) => y ≌ exr[Int, Int]
// now use product
{ (x:Int, y:Int) => x } ⨂ { (x:Int, y:Int) => y } ≌ (x:Int, y:Int) => (x, y)
// using projections it can be rewritten
exl[Int, Int] ⨂ exr[Int, Int] ≌ (x:Int, y:Int) => (x, y)
// now compose with + : (Int, Int) => Int
( + ) ○ { (x:Int, y:Int) => (x, y) } ≌ x + y
// or
plus ≌ ( + ) ○ (exl[Int, Int] ⨂ exr[Int, Int])