flip eq curry swap uncurry

Stream: Is there code for X?

[Adam Topaz]

I would be surprised if the following doesn't already exist, but I couldn't find it.

import category_theory.currying

open category_theory
variables {C D E : Type*} [category C] [category D] [category E]

example (F : C ⥤ D ⥤ E) :
  F.flip ≅ curry.obj (category_theory.prod.swap _ _ ⋙ uncurry.obj F) :=
nat_iso.of_components (λ d, nat_iso.of_components (λ c, eq_to_iso rfl) $ by tidy) $ by tidy

[Adam Topaz]

#11151