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).

This is used in CategoryTheory.Category.Cat.CartesianClosed to equip the category of small categories Cat.{u, u} with a Cartesian closed structure.

def CategoryTheory.Functor.uncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor (Functor C (Functor D E)) (Functor (C × D) E)

The uncurrying functor, taking a functor C ⥤ (D ⥤ E) and producing a functor (C × D) ⥤ E.

@[simp]

theorem CategoryTheory.Functor.uncurry_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X ⟶ Y) : (uncurry.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)

@[simp]

theorem CategoryTheory.Functor.uncurry_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (T : X✝ ⟶ Y✝) (X : C × D) : (uncurry.map T).app X = (T.app X.1).app X.2

@[simp]

theorem CategoryTheory.Functor.uncurry_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) : (uncurry.obj F).obj X = (F.obj X.1).obj X.2

def CategoryTheory.Functor.curryObj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) : Functor C (Functor D E)

The object level part of the currying functor. (See curry for the functorial version.)

def CategoryTheory.Functor.curry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor (Functor (C × D) E) (Functor C (Functor D E))

The currying functor, taking a functor (C × D) ⥤ E and producing a functor C ⥤ (D ⥤ E).

@[simp]

theorem CategoryTheory.Functor.curry_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) (Y : D) : ((curry.obj F).obj X).obj Y = F.obj (X, Y)

@[simp]

theorem CategoryTheory.Functor.curry_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor (C × D) E} (T : X✝ ⟶ Y✝) (X : C) (Y : D) : ((curry.map T).app X).app Y = T.app (X, Y)

@[simp]

theorem CategoryTheory.Functor.curry_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((curry.obj F).map f).app Y = F.map (Prod.mkHom f (CategoryStruct.id Y))

@[simp]

theorem CategoryTheory.Functor.curry_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((curry.obj F).obj X).map g = F.map (Prod.mkHom (CategoryStruct.id X) g)

def CategoryTheory.Functor.currying {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor C (Functor D E) ≌ Functor (C × D) E

The equivalence of functor categories given by currying/uncurrying.

@[simp]

theorem CategoryTheory.Functor.currying_functor_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) : (currying.functor.obj F).obj X = (F.obj X.1).obj X.2

@[simp]

theorem CategoryTheory.Functor.currying_functor_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (T : X✝ ⟶ Y✝) (X : C × D) : (currying.functor.map T).app X = (T.app X.1).app X.2

@[simp]

theorem CategoryTheory.Functor.currying_unitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝¹ : D) : ((currying.unitIso.inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.currying_inverse_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((currying.inverse.obj F).map f).app Y = F.map (Prod.mkHom f (CategoryStruct.id Y))

@[simp]

theorem CategoryTheory.Functor.currying_functor_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X ⟶ Y) : (currying.functor.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)

@[simp]

theorem CategoryTheory.Functor.currying_inverse_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor (C × D) E} (T : X✝ ⟶ Y✝) (X : C) (Y : D) : ((currying.inverse.map T).app X).app Y = T.app (X, Y)

@[simp]

theorem CategoryTheory.Functor.currying_counitIso_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor (C × D) E) (X✝ : C × D) : (currying.counitIso.hom.app X).app X✝ = CategoryStruct.id (X.obj (X✝.1, X✝.2))

@[simp]

theorem CategoryTheory.Functor.currying_inverse_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) (Y : D) : ((currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)

@[simp]

theorem CategoryTheory.Functor.currying_counitIso_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor (C × D) E) (X✝ : C × D) : (currying.counitIso.inv.app X).app X✝ = CategoryStruct.id (X.obj (X✝.1, X✝.2))

@[simp]

theorem CategoryTheory.Functor.currying_unitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝¹ : D) : ((currying.unitIso.hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.currying_inverse_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((currying.inverse.obj F).obj X).map g = F.map (Prod.mkHom (CategoryStruct.id X) g)

def CategoryTheory.Functor.flipping {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor C (Functor D E) ≌ Functor D (Functor C E)

The equivalence of functor categories given by flipping.

@[simp]

theorem CategoryTheory.Functor.flipping_unitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝¹ : D) : ((flipping.unitIso.inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.flipping_inverse_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) : ((flipping.inverse.obj F).map f).app j = (F.obj j).map f

@[simp]

theorem CategoryTheory.Functor.flipping_functor_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : ((flipping.functor.obj F).map f).app j = (F.obj j).map f

@[simp]

theorem CategoryTheory.Functor.flipping_functor_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) (j : C) : ((flipping.functor.obj F).obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flipping_functor_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor C (Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) : ((flipping.functor.map φ).app Y).app X = (φ.app X).app Y

@[simp]

theorem CategoryTheory.Functor.flipping_functor_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((flipping.functor.obj F).obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.Functor.flipping_counitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor D (Functor C E)) (X✝ : D) (X✝¹ : C) : ((flipping.counitIso.hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.flipping_inverse_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((flipping.inverse.obj F).obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.Functor.flipping_inverse_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) (j : D) : ((flipping.inverse.obj F).obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flipping_unitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝¹ : D) : ((flipping.unitIso.hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.flipping_counitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor D (Functor C E)) (X✝ : D) (X✝¹ : C) : ((flipping.counitIso.inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((X.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.flipping_inverse_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor D (Functor C E)} (φ : F₁ ⟶ F₂) (Y : C) (X : D) : ((flipping.inverse.map φ).app Y).app X = (φ.app X).app Y

def CategoryTheory.Functor.fullyFaithfulUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : uncurry.FullyFaithful

The functor uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E is fully faithful.

def CategoryTheory.Functor.fullyFaithfulCurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : curry.FullyFaithful

The functor curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E is fully faithful.

instance CategoryTheory.Functor.instFullProdCurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : curry.Full

instance CategoryTheory.Functor.instFaithfulProdCurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : curry.Faithful

instance CategoryTheory.Functor.instFullProdUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : uncurry.Full

instance CategoryTheory.Functor.instFaithfulProdUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : uncurry.Faithful

def CategoryTheory.Functor.curryObjProdComp {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{v_1, u_1} C'] [Category.{v_2, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) : curry.obj ((F₁.prod F₂).comp G) ≅ F₁.comp ((curry.obj G).comp ((whiskeringLeft C' D' E).obj F₂))

Given functors F₁ : C ⥤ D, F₂ : C' ⥤ D' and G : D × D' ⥤ E, this is the isomorphism between curry.obj ((F₁.prod F₂).comp G) and F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ in the category C ⥤ C' ⥤ E.

@[simp]

theorem CategoryTheory.Functor.curryObjProdComp_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{v_1, u_1} C'] [Category.{v_2, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) (X : C) (X✝ : C') : ((F₁.curryObjProdComp F₂ G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))

@[simp]

theorem CategoryTheory.Functor.curryObjProdComp_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{v_1, u_1} C'] [Category.{v_2, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) (X : C) (X✝ : C') : ((F₁.curryObjProdComp F₂ G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))

def CategoryTheory.Functor.flipIsoCurrySwapUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) : F.flip ≅ curry.obj ((Prod.swap D C).comp (uncurry.obj F))

F.flip is isomorphic to uncurrying F, swapping the variables, and currying.

@[simp]

theorem CategoryTheory.Functor.flipIsoCurrySwapUncurry_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D) (X✝ : C) : (F.flipIsoCurrySwapUncurry.inv.app X).app X✝ = CategoryStruct.id ((F.obj X✝).obj X)

@[simp]

theorem CategoryTheory.Functor.flipIsoCurrySwapUncurry_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D) (X✝ : C) : (F.flipIsoCurrySwapUncurry.hom.app X).app X✝ = CategoryStruct.id ((F.obj X✝).obj X)

def CategoryTheory.Functor.uncurryObjFlip {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) : uncurry.obj F.flip ≅ (Prod.swap D C).comp (uncurry.obj F)

The uncurrying of F.flip is isomorphic to swapping the factors followed by the uncurrying of F.

@[simp]

theorem CategoryTheory.Functor.uncurryObjFlip_hom_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D × C) : F.uncurryObjFlip.hom.app X = CategoryStruct.id ((F.obj X.2).obj X.1)

@[simp]

theorem CategoryTheory.Functor.uncurryObjFlip_inv_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D × C) : F.uncurryObjFlip.inv.app X = CategoryStruct.id ((F.obj X.2).obj X.1)

def CategoryTheory.Functor.whiskeringRight₂ (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] : Functor (Functor C (Functor D E)) (Functor (Functor B C) (Functor (Functor B D) (Functor B E)))

A version of CategoryTheory.whiskeringRight for bifunctors, obtained by uncurrying, applying whiskeringRight and currying back

@[simp]

theorem CategoryTheory.Functor.whiskeringRight₂_obj_obj_map_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) {X✝¹ Y✝ : Functor B D} (g : X✝¹ ⟶ Y✝) (X✝² : B) : ((((whiskeringRight₂ B C D E).obj X).obj X✝).map g).app X✝² = (X.obj (X✝.obj X✝²)).map (g.app X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringRight₂_map_app_app_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (f : X✝ ⟶ Y✝) (X : Functor B C) (Y : Functor B D) (c : B) : ((((whiskeringRight₂ B C D E).map f).app X).app Y).app c = (f.app (X.obj c)).app (Y.obj c)

@[simp]

theorem CategoryTheory.Functor.whiskeringRight₂_obj_obj_obj_map (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) (Y : Functor B D) {X✝¹ Y✝ : B} (f : X✝¹ ⟶ Y✝) : ((((whiskeringRight₂ B C D E).obj X).obj X✝).obj Y).map f = CategoryStruct.comp ((X.map (X✝.map f)).app (Y.obj X✝¹)) ((X.obj (X✝.obj Y✝)).map (Y.map f))

@[simp]

theorem CategoryTheory.Functor.whiskeringRight₂_obj_map_app_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) {X✝ Y✝ : Functor B C} (f : X✝ ⟶ Y✝) (Y : Functor B D) (X✝¹ : B) : ((((whiskeringRight₂ B C D E).obj X).map f).app Y).app X✝¹ = (X.map (f.app X✝¹)).app (Y.obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.whiskeringRight₂_obj_obj_obj_obj (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) (Y : Functor B D) (X✝¹ : B) : ((((whiskeringRight₂ B C D E).obj X).obj X✝).obj Y).obj X✝¹ = (X.obj (X✝.obj X✝¹)).obj (Y.obj X✝¹)

theorem CategoryTheory.Functor.uncurry_obj_curry_obj {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor (B × C) D) : uncurry.obj (curry.obj F) = F

theorem CategoryTheory.Functor.curry_obj_injective {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor (C × D) E} (h : curry.obj F₁ = curry.obj F₂) : F₁ = F₂

theorem CategoryTheory.Functor.curry_obj_uncurry_obj {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor B (Functor C D)) : curry.obj (uncurry.obj F) = F

theorem CategoryTheory.Functor.uncurry_obj_injective {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {F₁ F₂ : Functor B (Functor C D)} (h : uncurry.obj F₁ = uncurry.obj F₂) : F₁ = F₂

theorem CategoryTheory.Functor.flip_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor B (Functor C D)) : F.flip.flip = F

theorem CategoryTheory.Functor.flip_injective {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {F₁ F₂ : Functor B (Functor C D)} (h : F₁.flip = F₂.flip) : F₁ = F₂

theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {H : Type u₅} [Category.{v₅, u₅} H] (F₁ : Functor B C) (F₂ : Functor D E) (G : Functor (C × E) H) : uncurry.obj (F₂.comp (F₁.comp (curry.obj G)).flip).flip = (F₁.prod F₂).comp G

theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip' {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {H : Type u₅} [Category.{v₅, u₅} H] (F₁ : Functor B C) (F₂ : Functor D E) (G : Functor (C × E) H) : uncurry.obj (F₁.comp (F₂.comp (curry.obj G).flip).flip) = (F₁.prod F₂).comp G

def CategoryTheory.Functor.compFlipUncurryIso {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) : uncurry.obj (F.comp G).flip ≅ ((Functor.id C).prod F).comp (uncurry.obj G.flip)

Natural isomorphism witnessing comp_flip_uncurry_eq.

@[simp]

theorem CategoryTheory.Functor.compFlipUncurryIso_hom_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) (X : C × B) : (F.compFlipUncurryIso G).hom.app X = CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)

@[simp]

theorem CategoryTheory.Functor.compFlipUncurryIso_inv_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) (X : C × B) : (F.compFlipUncurryIso G).inv.app X = CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)

theorem CategoryTheory.Functor.comp_flip_uncurry_eq {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) : uncurry.obj (F.comp G).flip = ((Functor.id C).prod F).comp (uncurry.obj G.flip)

def CategoryTheory.Functor.curryObjCompIso {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) : (curry.obj (F.comp G)).flip ≅ (curry.obj F).flip.comp ((whiskeringRight C D E).obj G)

Natural isomorphism witnessing comp_flip_curry_eq.

@[simp]

theorem CategoryTheory.Functor.curryObjCompIso_hom_app_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) (X : B) (X✝ : C) : ((F.curryObjCompIso G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F.obj (X✝, X)))

@[simp]

theorem CategoryTheory.Functor.curryObjCompIso_inv_app_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) (X : B) (X✝ : C) : ((F.curryObjCompIso G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F.obj (X✝, X)))

theorem CategoryTheory.Functor.curry_obj_comp_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) : (curry.obj (F.comp G)).flip = (curry.obj F).flip.comp ((whiskeringRight C D E).obj G)

def CategoryTheory.Functor.flippingEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor C (Functor D E) ≃ Functor D (Functor C E)

The equivalence of types of bifunctors giving by flipping the arguments.

@[simp]

theorem CategoryTheory.Functor.flippingEquiv_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((flippingEquiv F).obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.Functor.flippingEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((flippingEquiv.symm F).obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.Functor.flippingEquiv_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) (j : C) : ((flippingEquiv F).obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flippingEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) (j : D) : ((flippingEquiv.symm F).obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flippingEquiv_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : ((flippingEquiv F).map f).app j = (F.obj j).map f

@[simp]

theorem CategoryTheory.Functor.flippingEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) : ((flippingEquiv.symm F).map f).app j = (F.obj j).map f

def CategoryTheory.Functor.curryingEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor C (Functor D E) ≃ Functor (C × D) E

The equivalence of types of bifunctors given by currying.

@[simp]

theorem CategoryTheory.Functor.curryingEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((curryingEquiv.symm G).map f).app Y = G.map (Prod.mkHom f (CategoryStruct.id Y))

@[simp]

theorem CategoryTheory.Functor.curryingEquiv_apply_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X ⟶ Y) : (curryingEquiv F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)

@[simp]

theorem CategoryTheory.Functor.curryingEquiv_apply_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) : (curryingEquiv F).obj X = (F.obj X.1).obj X.2

@[simp]

theorem CategoryTheory.Functor.curryingEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((curryingEquiv.symm G).obj X).map g = G.map (Prod.mkHom (CategoryStruct.id X) g)

@[simp]

theorem CategoryTheory.Functor.curryingEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) (X : C) (Y : D) : ((curryingEquiv.symm G).obj X).obj Y = G.obj (X, Y)

def CategoryTheory.Functor.curryingFlipEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] : Functor D (Functor C E) ≃ Functor (C × D) E

The flipped equivalence of types of bifunctors given by currying.

@[simp]

theorem CategoryTheory.Functor.curryingFlipEquiv_apply_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor D (Functor C E)) {X Y : C × D} (f : X ⟶ Y) : (curryingFlipEquiv a✝).map f = CategoryStruct.comp ((a✝.map f.2).app X.1) ((a✝.obj Y.2).map f.1)

@[simp]

theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((curryingFlipEquiv.symm a✝).obj k).map f = a✝.map (Prod.mkHom f (CategoryStruct.id k))

@[simp]

theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) (k : D) (j : C) : ((curryingFlipEquiv.symm a✝).obj k).obj j = a✝.obj (j, k)

@[simp]

theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : ((curryingFlipEquiv.symm a✝).map f).app j = a✝.map (Prod.mkHom (CategoryStruct.id j) f)

@[simp]

theorem CategoryTheory.Functor.curryingFlipEquiv_apply_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor D (Functor C E)) (X : C × D) : (curryingFlipEquiv a✝).obj X = (a✝.obj X.2).obj X.1