Currying of functors in three variables

We study the equivalence of categories currying₃ : (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E.

def CategoryTheory.Functor.currying₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor C₁ (Functor C₂ (Functor C₃ E)) ≌ Functor (C₁ × C₂ × C₃) E

The equivalence of categories (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E given by the curryfication of functors in three variables.

Equations

• CategoryTheory.Functor.currying₃ = CategoryTheory.Functor.currying.trans (CategoryTheory.Functor.currying.trans (CategoryTheory.prod.associativity C₁ C₂ C₃).congrLeft)

@[reducible, inline]

abbrev CategoryTheory.Functor.uncurry₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor (Functor C₁ (Functor C₂ (Functor C₃ E))) (Functor (C₁ × C₂ × C₃) E)

Uncurrying a functor in three variables.

Equations

• CategoryTheory.Functor.uncurry₃ = CategoryTheory.Functor.currying₃.functor

@[reducible, inline]

abbrev CategoryTheory.Functor.curry₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor (Functor (C₁ × C₂ × C₃) E) (Functor C₁ (Functor C₂ (Functor C₃ E)))

Currying a functor in three variables.

Equations

• CategoryTheory.Functor.curry₃ = CategoryTheory.Functor.currying₃.inverse

def CategoryTheory.Functor.fullyFaithfulUncurry₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : uncurry₃.FullyFaithful

Uncurrying functors in three variables gives a fully faithful functor.

Equations

• CategoryTheory.Functor.fullyFaithfulUncurry₃ = CategoryTheory.Functor.currying₃.fullyFaithfulFunctor

@[simp]

theorem CategoryTheory.Functor.curry₃_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor (C₁ × C₂ × C₃) E) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃) : (((curry₃.obj F).map f).app X₂).app X₃ = F.map (f, CategoryStruct.id X₂, CategoryStruct.id X₃)

@[simp]

theorem CategoryTheory.Functor.curry₃_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) {X₂ Y₂ : C₂} (f : X₂ ⟶ Y₂) (X₃ : C₃) : (((curry₃.obj F).obj X₁).map f).app X₃ = F.map (CategoryStruct.id X₁, f, CategoryStruct.id X₃)

@[simp]

theorem CategoryTheory.Functor.curry₃_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) (X₂ : C₂) {X₃ Y₃ : C₃} (f : X₃ ⟶ Y₃) : (((curry₃.obj F).obj X₁).obj X₂).map f = F.map (CategoryStruct.id X₁, CategoryStruct.id X₂, f)

@[simp]

theorem CategoryTheory.Functor.curry₃_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] {F G : Functor (C₁ × C₂ × C₃) E} (f : F ⟶ G) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((curry₃.map f).app X₁).app X₂).app X₃ = f.app (X₁, X₂, X₃)

@[simp]

theorem CategoryTheory.Functor.currying₃_unitIso_hom_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_13, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_11, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ = CategoryStruct.id (((((Functor.id (Functor C₁ (Functor C₂ (Functor C₃ E)))).obj F).obj X₁).obj X₂).obj X₃)

@[simp]

theorem CategoryTheory.Functor.currying₃_unitIso_inv_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_13, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_11, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ = CategoryStruct.id (((((currying₃.functor.comp currying₃.inverse).obj F).obj X₁).obj X₂).obj X₃)

def CategoryTheory.Functor.curry₃ObjProdComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_6} D₁] [Category.{u_14, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_16, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (G : Functor (D₁ × D₂ × D₃) E) : curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G) ≅ F₁.comp ((curry₃.obj G).comp (((whiskeringLeft₂ E).obj F₂).obj F₃))

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.curry₃ObjProdComp_hom_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_6} D₁] [Category.{u_14, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_16, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (G : Functor (D₁ × D₂ × D₃) E) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) : (((F₁.curry₃ObjProdComp F₂ F₃ G).hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((((curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.curry₃ObjProdComp_inv_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_6} D₁] [Category.{u_14, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_16, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (G : Functor (D₁ × D₂ × D₃) E) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) : (((F₁.curry₃ObjProdComp F₂ F₃ G).inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((((curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X✝).obj X✝¹)

def CategoryTheory.Functor.bifunctorComp₁₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_3} C₁₂] [Category.{u_14, u_9} E] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ E)) : bifunctorComp₁₂ F₁₂ G ≅ curry.obj ((uncurry.obj F₁₂).comp G)

bifunctorComp₁₂ can be described in terms of the curryfication of functors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.bifunctorComp₁₂Iso_inv_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_3} C₁₂] [Category.{u_14, u_9} E] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ E)) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) : (((F₁₂.bifunctorComp₁₂Iso G).inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((G.obj ((F₁₂.obj X).obj X✝)).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.bifunctorComp₁₂Iso_hom_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_3} C₁₂] [Category.{u_14, u_9} E] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ E)) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) : (((F₁₂.bifunctorComp₁₂Iso G).hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((G.obj ((F₁₂.obj X).obj X✝)).obj X✝¹)

def CategoryTheory.Functor.bifunctorComp₂₃Iso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_5} C₂₃] [Category.{u_14, u_9} E] (F : Functor C₁ (Functor C₂₃ E)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) : bifunctorComp₂₃ F G₂₃ ≅ curry.obj (curry.obj ((prod.associator C₁ C₂ C₃).comp (uncurry.obj ((uncurry.obj G₂₃).comp F.flip).flip)))

bifunctorComp₂₃ can be described in terms of the curryfication of functors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.bifunctorComp₂₃Iso_inv_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_5} C₂₃] [Category.{u_14, u_9} E] (F : Functor C₁ (Functor C₂₃ E)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) : (((F.bifunctorComp₂₃Iso G₂₃).inv.app X).app X✝).app X✝¹ = CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X✝).obj X✝¹))

@[simp]

theorem CategoryTheory.Functor.bifunctorComp₂₃Iso_hom_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_5} C₂₃] [Category.{u_14, u_9} E] (F : Functor C₁ (Functor C₂₃ E)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X : C₁) (X✝ : C₂) (X✝¹ : C₃) : (((F.bifunctorComp₂₃Iso G₂₃).hom.app X).app X✝).app X✝¹ = CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X✝).obj X✝¹))

def CategoryTheory.Functor.flip₁₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) : Functor C₃ (Functor C₂ (Functor C₁ E))

Flip the first and third arguments in a trifunctor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.flip₁₃_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {X✝ Y✝ : C₃} (h : X✝ ⟶ Y✝) (X : C₂) (Y : C₁) : ((F.flip₁₃.map h).app X).app Y = ((F.obj Y).obj X).map h

@[simp]

theorem CategoryTheory.Functor.flip₁₃_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₃) (H : C₂) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) : ((F.flip₁₃.obj G).obj H).map f = ((F.map f).app H).app G

@[simp]

theorem CategoryTheory.Functor.flip₁₃_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₃) {X✝ Y✝ : C₂} (g : X✝ ⟶ Y✝) (X : C₁) : ((F.flip₁₃.obj G).map g).app X = ((F.obj X).map g).app G

@[simp]

theorem CategoryTheory.Functor.flip₁₃_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₃) (H : C₂) (K : C₁) : ((F.flip₁₃.obj G).obj H).obj K = ((F.obj K).obj H).obj G

def CategoryTheory.Functor.flip₁₃Functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor (Functor C₁ (Functor C₂ (Functor C₃ E))) (Functor C₃ (Functor C₂ (Functor C₁ E)))

Flip the first and third arguments in a trifunctor, as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.flip₁₃Functor_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₃) {X✝ Y✝ : C₂} (g : X✝ ⟶ Y✝) (X : C₁) : (((flip₁₃Functor.obj F).obj G).map g).app X = ((F.obj X).map g).app G

@[simp]

theorem CategoryTheory.Functor.flip₁₃Functor_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₃) (H : C₂) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) : (((flip₁₃Functor.obj F).obj G).obj H).map f = ((F.map f).app H).app G

@[simp]

theorem CategoryTheory.Functor.flip₁₃Functor_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₃) (H : C₂) (K : C₁) : (((flip₁₃Functor.obj F).obj G).obj H).obj K = ((F.obj K).obj H).obj G

@[simp]

theorem CategoryTheory.Functor.flip₁₃Functor_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {X✝ Y✝ : C₃} (h : X✝ ⟶ Y✝) (X : C₂) (Y : C₁) : (((flip₁₃Functor.obj F).map h).app X).app Y = ((F.obj Y).obj X).map h

@[simp]

theorem CategoryTheory.Functor.flip₁₃Functor_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] {X✝ Y✝ : Functor C₁ (Functor C₂ (Functor C₃ E))} (f : X✝ ⟶ Y✝) (X : C₃) (Y : C₂) (Z : C₁) : (((flip₁₃Functor.map f).app X).app Y).app Z = ((f.app Z).app Y).app X

def CategoryTheory.Functor.flip₂₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) : Functor C₁ (Functor C₃ (Functor C₂ E))

Flip the second and third arguments in a trifunctor.

Equations

• F.flip₂₃ = { obj := fun (G : C₁) => (F.obj G).flip, map := fun {X Y : C₁} (f : X ⟶ Y) => (CategoryTheory.flipFunctor C₂ C₃ E).map (F.map f), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Functor.flip₂₃_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₁) (k : C₃) {X✝ Y✝ : C₂} (f : X✝ ⟶ Y✝) : ((F.flip₂₃.obj G).obj k).map f = ((F.obj G).map f).app k

@[simp]

theorem CategoryTheory.Functor.flip₂₃_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₁) {X✝ Y✝ : C₃} (f : X✝ ⟶ Y✝) (j : C₂) : ((F.flip₂₃.obj G).map f).app j = ((F.obj G).obj j).map f

@[simp]

theorem CategoryTheory.Functor.flip₂₃_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₁) (k : C₃) (j : C₂) : ((F.flip₂₃.obj G).obj k).obj j = ((F.obj G).obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flip₂₃_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (Y : C₃) (X : C₂) : ((F.flip₂₃.map f).app Y).app X = ((F.map f).app X).app Y

def CategoryTheory.Functor.flip₂₃Functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor (Functor C₁ (Functor C₂ (Functor C₃ E))) (Functor C₁ (Functor C₃ (Functor C₂ E)))

Flip the second and third arguments in a trifunctor, as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.flip₂₃Functor_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₁) (k : C₃) (j : C₂) : (((flip₂₃Functor.obj F).obj G).obj k).obj j = ((F.obj G).obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flip₂₃Functor_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (Y : C₃) (X : C₂) : (((flip₂₃Functor.obj F).map f).app Y).app X = ((F.map f).app X).app Y

@[simp]

theorem CategoryTheory.Functor.flip₂₃Functor_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₁) (k : C₃) {X✝ Y✝ : C₂} (f : X✝ ⟶ Y✝) : (((flip₂₃Functor.obj F).obj G).obj k).map f = ((F.obj G).map f).app k

@[simp]

theorem CategoryTheory.Functor.flip₂₃Functor_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (G : C₁) {X✝ Y✝ : C₃} (f : X✝ ⟶ Y✝) (j : C₂) : (((flip₂₃Functor.obj F).obj G).map f).app j = ((F.obj G).obj j).map f

@[simp]

theorem CategoryTheory.Functor.flip₂₃Functor_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] {X✝ Y✝ : Functor C₁ (Functor C₂ (Functor C₃ E))} (f : X✝ ⟶ Y✝) (X : C₁) (Y : C₃) (Z : C₂) : (((flip₂₃Functor.map f).app X).app Y).app Z = ((f.app X).app Z).app Y