0
$\begingroup$

I was studying the definition of currying and uncurrying using Category Theory from these slides. The answer and the proof on slide 19 makes 100% sense to me however, the definitions seem to come out of nowhere. This is what I seek to understand, how I could have come up with such answer (especially since the next exercise seems to require a similar intuitive thinking about this). I see that they satisfy the properties that we need in particular:

$$ curry(uncurry(f)) = f$$ $$ uncurry(curry(g)) = g$$

by defining $curry(f)$ to be the unique morphism $g$ that satisfies:

$$ f = app^{B,C} \circ (g \times 1_B) = (g \times 1_B); app^{B,C}$$

and $uncurry(g)$ to be morphism:

$$uncurry(g) = app^{B,C} \circ (g \times 1_B) = (g \times 1_B); app^{B,C}$$

however, how could I have known that that was the right mapping for the morphisms $f:A \times B \to C$ and $g: A \to (B\to C)$? I feel sometimes category theory is so abstract that it makes its unituitive to me how or where things come from. Especially why these definitions of currying and uncurrying actually work "the way they should".

$\endgroup$
  • 1
    $\begingroup$ This is just the equation produced by a (co-)universal arrow. The formula is a special case of a result that holds for any adjunction. (Here, $app$ is the counit of the adjunction.) $\endgroup$ – Derek Elkins Nov 22 '18 at 19:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.