- { g:(X* Y)-> Z}, that is, { g\in [(X* Y)-> Z]}
[A->B]} :space of f: A-> B. By #currying, { {{curry}}(g):X-> [Y->Z]}
Apply -> #morphism
{{Apply}}:([Y-> Z]* Y)->Z},
so
{ {{Apply}}(f,y)=f(y)}
Ie commuting diagram

{ {Apply}}\circ \left({{curry}}(g)\times {{id}}_{Y}\right)=g}