Curry and uncurry, as functors. #
The uncurrying functor, taking a functor
C ⥤ (D ⥤ E) and producing a functor
(C × D) ⥤ E.
The object level part of the currying functor. (See
curry for the functorial version.)
The currying functor, taking a functor
(C × D) ⥤ E and producing a functor
C ⥤ (D ⥤ E).
The equivalence of functor categories given by currying/uncurrying.
F.flip is isomorphic to uncurrying
F, swapping the variables, and currying.
The uncurrying of
F.flip is isomorphic to
swapping the factors followed by the uncurrying of
A version of
CategoryTheory.whiskeringRight for bifunctors, obtained by uncurrying,
whiskeringRight and currying back