Whiskering

Given a functor F : C ⥤ D and functors G H : D ⥤ E and a natural transformation α : G ⟶ H, we can construct a new natural transformation F ⋙ G ⟶ F ⋙ H, called whiskerLeft F α. This is the same as the horizontal composition of 𝟙 F with α.

This operation is functorial in F, and we package this as whiskeringLeft. Here (whiskeringLeft.obj F).obj G is F ⋙ G, and (whiskeringLeft.obj F).map α is whiskerLeft F α. (That is, we might have alternatively named this as the "left composition functor".)

We also provide analogues for composition on the right, and for these operations on isomorphisms.

We show the associator and unitor natural isomorphisms satisfy the triangle and pentagon identities.

def CategoryTheory.Functor.whiskerLeft {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.comp G ⟶ F.comp H

If α : G ⟶ H then whiskerLeft F α : F ⋙ G ⟶ F ⋙ H has components α.app (F.obj X).

@[simp]

theorem CategoryTheory.Functor.whiskerLeft_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) {G H : Functor D E} (α : G ⟶ H) (X : C) : (F.whiskerLeft α).app X = α.app (F.obj X)

@[simp]

theorem CategoryTheory.Functor.id_hcomp {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) : CategoryStruct.id F ◫ α = F.whiskerLeft α

def CategoryTheory.Functor.whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ⟶ H) (F : Functor D E) : G.comp F ⟶ H.comp F

If α : G ⟶ H then whiskerRight α F : G ⋙ F ⟶ H ⋙ F has components F.map (α.app X).

@[simp]

theorem CategoryTheory.Functor.whiskerRight_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ⟶ H) (F : Functor D E) (X : C) : (whiskerRight α F).app X = F.map (α.app X)

@[simp]

theorem CategoryTheory.Functor.hcomp_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ⟶ H) (F : Functor D E) : α ◫ CategoryStruct.id F = whiskerRight α F

def CategoryTheory.Functor.whiskeringLeft (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) (Functor (Functor D E) (Functor C E))

Left-composition gives a functor (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)).

(whiskeringLeft.obj F).obj G is F ⋙ G, and (whiskeringLeft.obj F).map α is whiskerLeft F α.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft_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) {X✝ Y✝ : Functor D E} (α : X✝ ⟶ Y✝) : ((whiskeringLeft C D E).obj F).map α = F.whiskerLeft α

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft_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} (τ : X✝ ⟶ Y✝) (H : Functor D E) (c : C) : (((whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft_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) (G : Functor D E) : ((whiskeringLeft C D E).obj F).obj G = F.comp G

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

Right-composition gives a functor (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)).

(whiskeringRight.obj H).obj F is F ⋙ H, and (whiskeringRight.obj H).map α is whiskerRight α H.

@[simp]

theorem CategoryTheory.Functor.whiskeringRight_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 D E} (τ : X✝ ⟶ Y✝) (F : Functor C D) (c : C) : (((whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)

@[simp]

theorem CategoryTheory.Functor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (H : Functor D E) (F : Functor C D) : ((whiskeringRight C D E).obj H).obj F = F.comp H

@[simp]

theorem CategoryTheory.Functor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (H : Functor D E) {X✝ Y✝ : Functor C D} (α : X✝ ⟶ Y✝) : ((whiskeringRight C D E).obj H).map α = whiskerRight α H

instance CategoryTheory.Functor.faithful_whiskeringRight_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 E} [F.Faithful] : ((whiskeringRight C D E).obj F).Faithful

def CategoryTheory.Functor.FullyFaithful.whiskeringRight {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [Category.{v_1, u_1} C] : ((Functor.whiskeringRight C D E).obj F).FullyFaithful

If F : D ⥤ E is fully faithful, then so is (whiskeringRight C D E).obj F : (C ⥤ D) ⥤ C ⥤ E.

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.whiskeringRight_preimage_app {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor D E} (hF : F.FullyFaithful) (C : Type u_1) [Category.{v_1, u_1} C] {X✝ Y✝ : Functor C D} (f : ((Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((Functor.whiskeringRight C D E).obj F).obj Y✝) (X : C) : ((hF.whiskeringRight C).preimage f).app X = hF.preimage (f.app X)

theorem CategoryTheory.Functor.whiskeringLeft_obj_id {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] : (whiskeringLeft C C E).obj (Functor.id C) = Functor.id (Functor C E)

def CategoryTheory.Functor.whiskeringLeftObjIdIso {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] : (whiskeringLeft C C E).obj (Functor.id C) ≅ Functor.id (Functor C E)

The isomorphism between left-whiskering on the identity functor and the identity of the functor between the resulting functor categories.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeftObjIdIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (X : Functor C E) (X✝ : C) : (whiskeringLeftObjIdIso.hom.app X).app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeftObjIdIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (X : Functor C E) (X✝ : C) : (whiskeringLeftObjIdIso.inv.app X).app X✝ = CategoryStruct.id (X.obj X✝)

theorem CategoryTheory.Functor.whiskeringLeft_obj_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {D' : Type u₄} [Category.{v₄, u₄} D'] (F : Functor C D) (G : Functor D D') : (whiskeringLeft C D' E).obj (F.comp G) = ((whiskeringLeft D D' E).obj G).comp ((whiskeringLeft C D E).obj F)

def CategoryTheory.Functor.whiskeringLeftObjCompIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {D' : Type u₄} [Category.{v₄, u₄} D'] (F : Functor C D) (G : Functor D D') : (whiskeringLeft C D' E).obj (F.comp G) ≅ ((whiskeringLeft D D' E).obj G).comp ((whiskeringLeft C D E).obj F)

The isomorphism between left-whiskering on the composition of functors and the composition of two left-whiskering applications.

@[simp]

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

@[simp]

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

theorem CategoryTheory.Functor.whiskeringRight_obj_id {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] : (whiskeringRight E C C).obj (Functor.id C) = Functor.id (Functor E C)

def CategoryTheory.Functor.whiskeringRightObjIdIso {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] : (whiskeringRight E C C).obj (Functor.id C) ≅ Functor.id (Functor E C)

The isomorphism between right-whiskering on the identity functor and the identity of the functor between the resulting functor categories.

@[simp]

theorem CategoryTheory.Functor.whiskeringRightObjIdIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (X : Functor E C) (X✝ : E) : (whiskeringRightObjIdIso.hom.app X).app X✝ = CategoryStruct.id (X.obj X✝)

@[simp]

theorem CategoryTheory.Functor.whiskeringRightObjIdIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {E : Type u₃} [Category.{v₃, u₃} E] (X : Functor E C) (X✝ : E) : (whiskeringRightObjIdIso.inv.app X).app X✝ = CategoryStruct.id (X.obj X✝)

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

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

The isomorphism between right-whiskering on the composition of functors and the composition of two right-whiskering applications.

@[simp]

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

@[simp]

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

instance CategoryTheory.Functor.full_whiskeringRight_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 E} [F.Faithful] [F.Full] : ((whiskeringRight C D E).obj F).Full

@[simp]

theorem CategoryTheory.Functor.whiskerLeft_id {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 : Functor D E} : F.whiskerLeft (NatTrans.id G) = NatTrans.id (F.comp G)

@[simp]

theorem CategoryTheory.Functor.whiskerLeft_id' {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 : Functor D E} : F.whiskerLeft (CategoryStruct.id G) = CategoryStruct.id (F.comp G)

@[simp]

theorem CategoryTheory.Functor.whiskerRight_id {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} (F : Functor D E) : whiskerRight (NatTrans.id G) F = NatTrans.id (G.comp F)

@[simp]

theorem CategoryTheory.Functor.whiskerRight_id' {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} (F : Functor D E) : whiskerRight (CategoryStruct.id G) F = CategoryStruct.id (G.comp F)

@[simp]

theorem CategoryTheory.Functor.whiskerLeft_comp {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 K : Functor D E} (α : G ⟶ H) (β : H ⟶ K) : F.whiskerLeft (CategoryStruct.comp α β) = CategoryStruct.comp (F.whiskerLeft α) (F.whiskerLeft β)

theorem CategoryTheory.Functor.whiskerLeft_comp_assoc {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 K : Functor D E} (α : G ⟶ H) (β : H ⟶ K) {Z : Functor C E} (h : F.comp K ⟶ Z) : CategoryStruct.comp (F.whiskerLeft (CategoryStruct.comp α β)) h = CategoryStruct.comp (F.whiskerLeft α) (CategoryStruct.comp (F.whiskerLeft β) h)

@[simp]

theorem CategoryTheory.Functor.whiskerRight_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H K : Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : Functor D E) : whiskerRight (CategoryStruct.comp α β) F = CategoryStruct.comp (whiskerRight α F) (whiskerRight β F)

theorem CategoryTheory.Functor.whiskerRight_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H K : Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : Functor D E) {Z : Functor C E} (h : K.comp F ⟶ Z) : CategoryStruct.comp (whiskerRight (CategoryStruct.comp α β) F) h = CategoryStruct.comp (whiskerRight α F) (CategoryStruct.comp (whiskerRight β F) h)

theorem CategoryTheory.Functor.whiskerLeft_comp_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} {H K : Functor D E} (α : F ⟶ G) (β : H ⟶ K) : CategoryStruct.comp (F.whiskerLeft β) (whiskerRight α K) = CategoryStruct.comp (whiskerRight α H) (G.whiskerLeft β)

theorem CategoryTheory.Functor.whiskerLeft_comp_whiskerRight_assoc {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} {H K : Functor D E} (α : F ⟶ G) (β : H ⟶ K) {Z : Functor C E} (h : G.comp K ⟶ Z) : CategoryStruct.comp (F.whiskerLeft β) (CategoryStruct.comp (whiskerRight α K) h) = CategoryStruct.comp (whiskerRight α H) (CategoryStruct.comp (G.whiskerLeft β) h)

theorem CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerLeft_comp_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} {H K : Functor D E} (α : F ⟶ G) (β : H ⟶ K) : α ◫ β = CategoryStruct.comp (F.whiskerLeft β) (whiskerRight α K)

theorem CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerRight_comp_whiskerLeft {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} {H K : Functor D E} (α : G ⟶ F) (β : K ⟶ H) : α ◫ β = CategoryStruct.comp (whiskerRight α K) (F.whiskerLeft β)

def CategoryTheory.Functor.isoWhiskerLeft {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.comp G ≅ F.comp H

If α : G ≅ H is a natural isomorphism then isoWhiskerLeft F α : (F ⋙ G) ≅ (F ⋙ H) has components α.app (F.obj X).

@[simp]

theorem CategoryTheory.Functor.isoWhiskerLeft_hom {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.isoWhiskerLeft α).hom = F.whiskerLeft α.hom

@[simp]

theorem CategoryTheory.Functor.isoWhiskerLeft_inv {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.isoWhiskerLeft α).inv = F.whiskerLeft α.inv

theorem CategoryTheory.Functor.isoWhiskerLeft_symm {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.isoWhiskerLeft α).symm = F.isoWhiskerLeft α.symm

@[simp]

theorem CategoryTheory.Functor.isoWhiskerLeft_refl {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 : Functor D E) : F.isoWhiskerLeft (Iso.refl G) = Iso.refl (F.comp G)

def CategoryTheory.Functor.isoWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ≅ H) (F : Functor D E) : G.comp F ≅ H.comp F

If α : G ≅ H then isoWhiskerRight α F : (G ⋙ F) ≅ (H ⋙ F) has components F.map_iso (α.app X).

@[simp]

theorem CategoryTheory.Functor.isoWhiskerRight_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ≅ H) (F : Functor D E) : (isoWhiskerRight α F).hom = whiskerRight α.hom F

@[simp]

theorem CategoryTheory.Functor.isoWhiskerRight_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ≅ H) (F : Functor D E) : (isoWhiskerRight α F).inv = whiskerRight α.inv F

theorem CategoryTheory.Functor.isoWhiskerRight_symm {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ≅ H) (F : Functor D E) : (isoWhiskerRight α F).symm = isoWhiskerRight α.symm F

@[simp]

theorem CategoryTheory.Functor.isoWhiskerRight_refl {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 : Functor D E) : isoWhiskerRight (Iso.refl F) G = Iso.refl (F.comp G)

instance CategoryTheory.Functor.isIso_whiskerLeft {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) [IsIso α] : IsIso (F.whiskerLeft α)

instance CategoryTheory.Functor.isIso_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ⟶ H) (F : Functor D E) [IsIso α] : IsIso (whiskerRight α F)

@[simp]

theorem CategoryTheory.Functor.inv_whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H : Functor C D} (α : G ⟶ H) (F : Functor D E) [IsIso α] : CategoryTheory.inv (whiskerRight α F) = whiskerRight (CategoryTheory.inv α) F

@[simp]

theorem CategoryTheory.Functor.inv_whiskerLeft {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) [IsIso α] : CategoryTheory.inv (F.whiskerLeft α) = F.whiskerLeft (CategoryTheory.inv α)

@[simp]

theorem CategoryTheory.Functor.isoWhiskerLeft_trans {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 K : Functor D E} (α : G ≅ H) (β : H ≅ K) : F.isoWhiskerLeft (α ≪≫ β) = F.isoWhiskerLeft α ≪≫ F.isoWhiskerLeft β

theorem CategoryTheory.Functor.isoWhiskerLeft_trans_assoc {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 K : Functor D E} (α : G ≅ H) (β : H ≅ K) {Z : Functor C E} (h : F.comp K ≅ Z) : F.isoWhiskerLeft (α ≪≫ β) ≪≫ h = F.isoWhiskerLeft α ≪≫ F.isoWhiskerLeft β ≪≫ h

@[simp]

theorem CategoryTheory.Functor.isoWhiskerRight_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H K : Functor C D} (α : G ≅ H) (β : H ≅ K) (F : Functor D E) : isoWhiskerRight (α ≪≫ β) F = isoWhiskerRight α F ≪≫ isoWhiskerRight β F

theorem CategoryTheory.Functor.isoWhiskerRight_trans_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {G H K : Functor C D} (α : G ≅ H) (β : H ≅ K) (F : Functor D E) {Z : Functor C E} (h : K.comp F ≅ Z) : isoWhiskerRight (α ≪≫ β) F ≪≫ h = isoWhiskerRight α F ≪≫ isoWhiskerRight β F ≪≫ h

theorem CategoryTheory.Functor.isoWhiskerLeft_trans_isoWhiskerRight {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} {H K : Functor D E} (α : F ≅ G) (β : H ≅ K) : F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β

theorem CategoryTheory.Functor.isoWhiskerLeft_trans_isoWhiskerRight_assoc {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} {H K : Functor D E} (α : F ≅ G) (β : H ≅ K) {Z : Functor C E} (h : G.comp K ≅ Z) : F.isoWhiskerLeft β ≪≫ isoWhiskerRight α K ≪≫ h = isoWhiskerRight α H ≪≫ G.isoWhiskerLeft β ≪≫ h

@[simp]

theorem CategoryTheory.Functor.whiskerLeft_twice {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) (G : Functor C D) {H K : Functor D E} (α : H ⟶ K) : F.whiskerLeft (G.whiskerLeft α) = CategoryStruct.comp (F.associator G H).inv (CategoryStruct.comp ((F.comp G).whiskerLeft α) (F.associator G K).hom)

@[simp]

theorem CategoryTheory.Functor.whiskerRight_twice {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] {H K : Functor B C} (F : Functor C D) (G : Functor D E) (α : H ⟶ K) : whiskerRight (whiskerRight α F) G = CategoryStruct.comp (H.associator F G).hom (CategoryStruct.comp (whiskerRight α (F.comp G)) (K.associator F G).inv)

theorem CategoryTheory.Functor.whiskerRight_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) {G H : Functor C D} (α : G ⟶ H) (K : Functor D E) : whiskerRight (F.whiskerLeft α) K = CategoryStruct.comp (F.associator G K).hom (CategoryStruct.comp (F.whiskerLeft (whiskerRight α K)) (F.associator H K).inv)

@[simp]

theorem CategoryTheory.Functor.isoWhiskerLeft_twice {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) (G : Functor C D) {H K : Functor D E} (α : H ≅ K) : F.isoWhiskerLeft (G.isoWhiskerLeft α) = (F.associator G H).symm ≪≫ (F.comp G).isoWhiskerLeft α ≪≫ F.associator G K

@[simp]

theorem CategoryTheory.Functor.isoWhiskerRight_twice {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] {H K : Functor B C} (F : Functor C D) (G : Functor D E) (α : H ≅ K) : isoWhiskerRight (isoWhiskerRight α F) G = H.associator F G ≪≫ isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm

theorem CategoryTheory.Functor.isoWhiskerRight_twice_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] {H K : Functor B C} (F : Functor C D) (G : Functor D E) (α : H ≅ K) {Z : Functor B E} (h : (K.comp F).comp G ≅ Z) : isoWhiskerRight (isoWhiskerRight α F) G ≪≫ h = H.associator F G ≪≫ isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm ≪≫ h

theorem CategoryTheory.Functor.isoWhiskerRight_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) {G H : Functor C D} (α : G ≅ H) (K : Functor D E) : isoWhiskerRight (F.isoWhiskerLeft α) K = F.associator G K ≪≫ F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ (F.associator H K).symm

theorem CategoryTheory.Functor.isoWhiskerRight_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) {G H : Functor C D} (α : G ≅ H) (K : Functor D E) {Z : Functor B E} (h : (F.comp H).comp K ≅ Z) : isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ h = F.associator G K ≪≫ F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ (F.associator H K).symm ≪≫ h

theorem CategoryTheory.Functor.isoWhiskerLeft_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) {G H : Functor C D} (α : G ≅ H) (K : Functor D E) : F.isoWhiskerLeft (isoWhiskerRight α K) = (F.associator G K).symm ≪≫ isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K

theorem CategoryTheory.Functor.isoWhiskerLeft_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {B : Type u₄} [Category.{v₄, u₄} B] (F : Functor B C) {G H : Functor C D} (α : G ≅ H) (K : Functor D E) {Z : Functor B E} (h : F.comp (H.comp K) ≅ Z) : F.isoWhiskerLeft (isoWhiskerRight α K) ≪≫ h = (F.associator G K).symm ≪≫ isoWhiskerRight (F.isoWhiskerLeft α) K ≪≫ F.associator H K ≪≫ h

theorem CategoryTheory.Functor.triangleIso {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor B C) : F.associator (Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor = isoWhiskerRight F.rightUnitor G

theorem CategoryTheory.Functor.triangleIso_assoc {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor B C) {Z : Functor A C} (h : F.comp G ≅ Z) : F.associator (Functor.id B) G ≪≫ F.isoWhiskerLeft G.leftUnitor ≪≫ h = isoWhiskerRight F.rightUnitor G ≪≫ h

theorem CategoryTheory.Functor.pentagonIso {A : Type u₁} [Category.{v₁, u₁} A] {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 A B) (G : Functor B C) (H : Functor C D) (K : Functor D E) : isoWhiskerRight (F.associator G H) K ≪≫ F.associator (G.comp H) K ≪≫ F.isoWhiskerLeft (G.associator H K) = (F.comp G).associator H K ≪≫ F.associator G (H.comp K)

theorem CategoryTheory.Functor.pentagonIso_assoc {A : Type u₁} [Category.{v₁, u₁} A] {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 A B) (G : Functor B C) (H : Functor C D) (K : Functor D E) {Z : Functor A E} (h : F.comp (G.comp (H.comp K)) ≅ Z) : isoWhiskerRight (F.associator G H) K ≪≫ F.associator (G.comp H) K ≪≫ F.isoWhiskerLeft (G.associator H K) ≪≫ h = (F.comp G).associator H K ≪≫ F.associator G (H.comp K) ≪≫ h

theorem CategoryTheory.Functor.triangle {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {C : Type u₃} [Category.{v₃, u₃} C] (F : Functor A B) (G : Functor B C) : CategoryStruct.comp (F.associator (Functor.id B) G).hom (F.whiskerLeft G.leftUnitor.hom) = whiskerRight F.rightUnitor.hom G

theorem CategoryTheory.Functor.pentagon {A : Type u₁} [Category.{v₁, u₁} A] {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 A B) (G : Functor B C) (H : Functor C D) (K : Functor D E) : CategoryStruct.comp (whiskerRight (F.associator G H).hom K) (CategoryStruct.comp (F.associator (G.comp H) K).hom (F.whiskerLeft (G.associator H K).hom)) = CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom

def CategoryTheory.Functor.whiskeringLeft₂ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] : Functor (Functor C₁ D₁) (Functor (Functor C₂ D₂) (Functor (Functor D₁ (Functor D₂ E)) (Functor C₁ (Functor C₂ E))))

The obvious functor (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E).

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (X : Functor D₁ (Functor D₂ E)) (X✝ : C₁) (X✝¹ : C₂) : (((((whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).obj X✝¹ = (X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₂_obj_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) {X✝ Y✝ : Functor D₁ (Functor D₂ E)} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) : (((((whiskeringLeft₂ E).obj F₁).obj F₂).map f).app X).app X✝¹ = (f.app (F₁.obj X)).app (F₂.obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (X : Functor D₁ (Functor D₂ E)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) : (((((whiskeringLeft₂ E).obj F₁).obj F₂).obj X).map f).app X✝¹ = (X.map (F₁.map f)).app (F₂.obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₂_obj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) {X✝ Y✝ : Functor C₂ D₂} (φ : X✝ ⟶ Y✝) (X : Functor D₁ (Functor D₂ E)) (X✝¹ : C₁) (c : C₂) : (((((whiskeringLeft₂ E).obj F₁).map φ).app X).app X✝¹).app c = (X.obj (F₁.obj X✝¹)).map (φ.app c)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₂_map_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] {X✝ Y✝ : Functor C₁ D₁} (ψ : X✝ ⟶ Y✝) (F₂ : Functor C₂ D₂) (X : Functor D₁ (Functor D₂ E)) (c : C₁) (X✝¹ : C₂) : (((((whiskeringLeft₂ E).map ψ).app F₂).app X).app c).app X✝¹ = (X.map (ψ.app c)).app (F₂.obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₂_obj_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (X : Functor D₁ (Functor D₂ E)) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) : (((((whiskeringLeft₂ E).obj F₁).obj F₂).obj X).obj X✝).map f = (X.obj (F₁.obj X✝)).map (F₂.map f)

def CategoryTheory.Functor.whiskeringLeft₃ObjObjObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) : Functor (Functor D₁ (Functor D₂ (Functor D₃ E))) (Functor C₁ (Functor C₂ (Functor C₃ E)))

Auxiliary definition for whiskeringLeft₃.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) (X✝² : C₃) : ((((whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).obj X✝¹).obj X✝² = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).obj (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : ((((whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).obj X✝¹).map f = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).map (F₃.map f)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : ((((whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).map f).app X✝¹).app X✝² = ((X.map (F₁.map f)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) {X✝ Y✝ : Functor D₁ (Functor D₂ (Functor D₃ E))} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) (X✝² : C₃) : ((((whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).map f).app X).app X✝¹).app X✝² = ((f.app (F₁.obj X)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObjObj_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : ((((whiskeringLeft₃ObjObjObj E F₁ F₂ F₃).obj X).obj X✝).map f).app X✝² = ((X.obj (F₁.obj X✝)).map (F₂.map f)).app (F₃.obj X✝²)

def CategoryTheory.Functor.whiskeringLeft₃ObjObjMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) {F₃ F₃' : Functor C₃ D₃} (τ₃ : F₃ ⟶ F₃') : whiskeringLeft₃ObjObjObj E F₁ F₂ F₃ ⟶ whiskeringLeft₃ObjObjObj E F₁ F₂ F₃'

Auxiliary definition for whiskeringLeft₃.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObjMap_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) {F₃ F₃' : Functor C₃ D₃} (τ₃ : F₃ ⟶ F₃') (F : Functor D₁ (Functor D₂ (Functor D₃ E))) : (whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃).app F = F₁.whiskerLeft (F.whiskerLeft (((whiskeringLeft₂ E).obj F₂).map τ₃))

def CategoryTheory.Functor.whiskeringLeft₃ObjObj {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) : Functor (Functor C₃ D₃) (Functor (Functor D₁ (Functor D₂ (Functor D₃ E))) (Functor C₁ (Functor C₂ (Functor C₃ E))))

Auxiliary definition for whiskeringLeft₃.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObj_obj {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) : (whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).obj F₃ = whiskeringLeft₃ObjObjObj E F₁ F₂ F₃

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjObj_map {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) {X✝ Y✝ : Functor C₃ D₃} (τ₃ : X✝ ⟶ Y✝) : (whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂).map τ₃ = whiskeringLeft₃ObjObjMap E F₁ F₂ τ₃

def CategoryTheory.Functor.whiskeringLeft₃ObjMap {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) {F₂ F₂' : Functor C₂ D₂} (τ₂ : F₂ ⟶ F₂') : whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂ ⟶ whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂'

Auxiliary definition for whiskeringLeft₃.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃ObjMap_app {C₁ : Type u_1} {C₂ : Type u_2} (C₃ : Type u_3) {D₁ : Type u_4} {D₂ : Type u_5} (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) {F₂ F₂' : Functor C₂ D₂} (τ₂ : F₂ ⟶ F₂') (F₃ : Functor C₃ D₃) : (whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂).app F₃ = whiskerRight ((whiskeringRight D₁ (Functor D₂ (Functor D₃ E)) (Functor C₂ (Functor C₃ E))).map (((whiskeringLeft₂ E).map τ₂).app F₃)) ((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ E))).obj F₁)

def CategoryTheory.Functor.whiskeringLeft₃Obj {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) : Functor (Functor C₂ D₂) (Functor (Functor C₃ D₃) (Functor (Functor D₁ (Functor D₂ (Functor D₃ E))) (Functor C₁ (Functor C₂ (Functor C₃ E)))))

Auxiliary definition for whiskeringLeft₃.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃Obj_map {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) {X✝ Y✝ : Functor C₂ D₂} (τ₂ : X✝ ⟶ Y✝) : (whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).map τ₂ = whiskeringLeft₃ObjMap C₃ D₃ E F₁ τ₂

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃Obj_obj {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) : (whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁).obj F₂ = whiskeringLeft₃ObjObj C₃ D₃ E F₁ F₂

def CategoryTheory.Functor.whiskeringLeft₃Map {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] {F₁ F₁' : Functor C₁ D₁} (τ₁ : F₁ ⟶ F₁') : whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁ ⟶ whiskeringLeft₃Obj C₂ C₃ D₂ D₃ E F₁'

Auxiliary definition for whiskeringLeft₃.

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃Map_app_app {C₁ : Type u_1} (C₂ : Type u_2) (C₃ : Type u_3) {D₁ : Type u_4} (D₂ : Type u_5) (D₃ : Type u_6) [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] {F₁ F₁' : Functor C₁ D₁} (τ₁ : F₁ ⟶ F₁') (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) : ((whiskeringLeft₃Map C₂ C₃ D₂ D₃ E τ₁).app F₂).app F₃ = ((whiskeringRight D₁ (Functor D₂ (Functor D₃ E)) (Functor C₂ (Functor C₃ E))).obj (((whiskeringLeft₂ E).obj F₂).obj F₃)).whiskerLeft ((whiskeringLeft C₁ D₁ (Functor C₂ (Functor C₃ E))).map τ₁)

def CategoryTheory.Functor.whiskeringLeft₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] : Functor (Functor C₁ D₁) (Functor (Functor C₂ D₂) (Functor (Functor C₃ D₃) (Functor (Functor D₁ (Functor D₂ (Functor D₃ E))) (Functor C₁ (Functor C₂ (Functor C₃ E))))))

The obvious functor (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (C₃ ⥤ D₃) ⥤ (D₁ ⥤ D₂ ⥤ D₃ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E).

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : (((((((whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).map f).app X✝² = ((X.obj (F₁.obj X✝)).map (F₂.map f)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_map_app_app_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] {X✝ Y✝ : Functor C₁ D₁} (τ₁ : X✝ ⟶ Y✝) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (c : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((whiskeringLeft₃ E).map τ₁).app F₂).app F₃).app X).app c).app X✝¹).app X✝² = ((X.map (τ₁.app c)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_map_app_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) {X✝ Y✝ : Functor C₂ D₂} (τ₂ : X✝ ⟶ Y✝) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝¹ : C₁) (c : C₂) (X✝² : C₃) : (((((((whiskeringLeft₃ E).obj F₁).map τ₂).app F₃).app X).app X✝¹).app c).app X✝² = ((X.obj (F₁.obj X✝¹)).map (τ₂.app c)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) {X✝ Y✝ : Functor D₁ (Functor D₂ (Functor D₃ E))} (f : X✝ ⟶ Y✝) (X : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).map f).app X).app X✝¹).app X✝² = ((f.app (F₁.obj X)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : (((((((whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).obj X✝¹).map f = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).map (F₃.map f)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : (((((((whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).map f).app X✝¹).app X✝² = ((X.map (F₁.map f)).app (F₂.obj X✝¹)).app (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (X : Functor D₁ (Functor D₂ (Functor D₃ E))) (X✝ : C₁) (X✝¹ : C₂) (X✝² : C₃) : (((((((whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X✝).obj X✝¹).obj X✝² = ((X.obj (F₁.obj X✝)).obj (F₂.obj X✝¹)).obj (F₃.obj X✝²)

@[simp]

theorem CategoryTheory.Functor.whiskeringLeft₃_obj_obj_map_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] (E : Type u_7) [Category.{v_7, u_7} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) {X✝ Y✝ : Functor C₃ D₃} (τ₃ : X✝ ⟶ Y✝) (F : Functor D₁ (Functor D₂ (Functor D₃ E))) (X : C₁) (X✝¹ : C₂) (c : C₃) : (((((((whiskeringLeft₃ E).obj F₁).obj F₂).map τ₃).app F).app X).app X✝¹).app c = ((F.obj (F₁.obj X)).obj (F₂.obj X✝¹)).map (τ₃.app c)

def CategoryTheory.Functor.postcompose₂ {C₁ : Type u_1} {C₂ : Type u_2} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] : Functor (Functor E E') (Functor (Functor C₁ (Functor C₂ E)) (Functor C₁ (Functor C₂ E')))

The "postcomposition" with a functor E ⥤ E' gives a functor (E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ E'.

@[simp]

theorem CategoryTheory.Functor.postcompose₂_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ E)) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) : (((postcompose₂.obj X).obj F).map f).app X✝¹ = X.map ((F.map f).app X✝¹)

@[simp]

theorem CategoryTheory.Functor.postcompose₂_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ E)) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) : (((postcompose₂.obj X).obj F).obj X✝).map f = X.map ((F.obj X✝).map f)

@[simp]

theorem CategoryTheory.Functor.postcompose₂_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ E)) (X✝ : C₁) (X✝¹ : C₂) : (((postcompose₂.obj X).obj F).obj X✝).obj X✝¹ = X.obj ((F.obj X✝).obj X✝¹)

@[simp]

theorem CategoryTheory.Functor.postcompose₂_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] {X✝ Y✝ : Functor E E'} (f : X✝ ⟶ Y✝) (F : Functor C₁ (Functor C₂ E)) (c : C₁) (c✝ : C₂) : (((postcompose₂.map f).app F).app c).app c✝ = f.app ((F.obj c).obj c✝)

@[simp]

theorem CategoryTheory.Functor.postcompose₂_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') {X✝ Y✝ : Functor C₁ (Functor C₂ E)} (α : X✝ ⟶ Y✝) (X✝¹ : C₁) (X✝² : C₂) : (((postcompose₂.obj X).map α).app X✝¹).app X✝² = X.map ((α.app X✝¹).app X✝²)

def CategoryTheory.Functor.postcompose₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] : Functor (Functor E E') (Functor (Functor C₁ (Functor C₂ (Functor C₃ E))) (Functor C₁ (Functor C₂ (Functor C₃ E'))))

The "postcomposition" with a functor E ⥤ E' gives a functor (E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E'.

@[simp]

theorem CategoryTheory.Functor.postcompose₃_obj_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X✝ : C₁) {X✝¹ Y✝ : C₂} (f : X✝¹ ⟶ Y✝) (X✝² : C₃) : ((((postcompose₃.obj X).obj F).obj X✝).map f).app X✝² = X.map (((F.obj X✝).map f).app X✝²)

@[simp]

theorem CategoryTheory.Functor.postcompose₃_map_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] {X✝ Y✝ : Functor E E'} (f : X✝ ⟶ Y✝) (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (c : C₁) (c✝ : C₂) (c✝¹ : C₃) : ((((postcompose₃.map f).app F).app c).app c✝).app c✝¹ = f.app (((F.obj c).obj c✝).obj c✝¹)

@[simp]

theorem CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X✝ : C₁) (X✝¹ : C₂) (X✝² : C₃) : ((((postcompose₃.obj X).obj F).obj X✝).obj X✝¹).obj X✝² = X.obj (((F.obj X✝).obj X✝¹).obj X✝²)

@[simp]

theorem CategoryTheory.Functor.postcompose₃_obj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') {X✝ Y✝ : Functor C₁ (Functor C₂ (Functor C₃ E))} (α : X✝ ⟶ Y✝) (X✝¹ : C₁) (X✝² : C₂) (X✝³ : C₃) : ((((postcompose₃.obj X).map α).app X✝¹).app X✝²).app X✝³ = X.map (((α.app X✝¹).app X✝²).app X✝³)

@[simp]

theorem CategoryTheory.Functor.postcompose₃_obj_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ (Functor C₃ E))) {X✝ Y✝ : C₁} (f : X✝ ⟶ Y✝) (X✝¹ : C₂) (X✝² : C₃) : ((((postcompose₃.obj X).obj F).map f).app X✝¹).app X✝² = X.map (((F.map f).app X✝¹).app X✝²)

@[simp]

theorem CategoryTheory.Functor.postcompose₃_obj_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] {E : Type u_7} [Category.{v_7, u_7} E] {E' : Type u_8} [Category.{v_8, u_8} E'] (X : Functor E E') (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X✝ : C₁) (X✝¹ : C₂) {X✝² Y✝ : C₃} (f : X✝² ⟶ Y✝) : ((((postcompose₃.obj X).obj F).obj X✝).obj X✝¹).map f = X.map (((F.obj X✝).obj X✝¹).map f)