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