@[simp]

theorem CategoryTheory.Functor.whiskerLeft_eqToHom {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) {G H : Functor D E} (η : G = H) : F.whiskerLeft (eqToHom η) = eqToHom ⋯

@[simp]

theorem CategoryTheory.Functor.eqToHom_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} (η : F = G) (H : Functor D E) : whiskerRight (eqToHom η) H = eqToHom ⋯

def CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (F : Functor C A) (G : Functor B D) : Functor (Functor A B) (Functor C D)

The functor that, on objects H : A ⥤ B acts by composing left and right with functors F ⋙ H ⋙ G F A <--------- C | . | | | . H | | whiskeringLeftObjWhiskeringRightObj.obj H | . V V B ----------> D G

Equations

• F.whiskeringLeftObjWhiskeringRightObj G = ((CategoryTheory.Functor.whiskeringLeft C A B).obj F).comp ((CategoryTheory.Functor.whiskeringRight C B D).obj G)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_obj {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_7, u_3} C] [Category.{u_8, u_4} D] (F : Functor C A) (G : Functor B D) (S : Functor A B) : (F.whiskeringLeftObjWhiskeringRightObj G).obj S = F.comp (S.comp G)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_map {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Category.{u_8, u_3} C] [Category.{u_7, u_4} D] (F : Functor C A) (G : Functor B D) {S1 S2 : Functor A B} (η : S1 ⟶ S2) : (F.whiskeringLeftObjWhiskeringRightObj G).map η = whiskerRight (F.whiskerLeft η) G

@[simp]

theorem CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_id_id {A : Type u_1} {B : Type u_2} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] : (Functor.id A).whiskeringLeftObjWhiskeringRightObj (Functor.id B) = Functor.id (Functor A B)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeftObjWhiskeringRightObj_comp_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [Category.{u_11, u_1} A] [Category.{u_12, u_2} B] [Category.{u_9, u_3} C] [Category.{u_10, u_4} D] (F : Functor C A) (G : Functor B D) {C' : Type u_5} {D' : Type u_6} [Category.{u_7, u_5} C'] [Category.{u_8, u_6} D'] (F' : Functor C' C) (G' : Functor D D') : (F'.comp F).whiskeringLeftObjWhiskeringRightObj (G.comp G') = (F.whiskeringLeftObjWhiskeringRightObj G).comp (F'.whiskeringLeftObjWhiskeringRightObj G')