Documentation

Mathlib.CategoryTheory.Whiskering

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.

At the end of the file, we provide the left and right unitors, and the associator, for functor composition. (In fact functor composition is definitionally associative, but very often relying on this causes extremely slow elaboration, so it is better to insert it explicitly.) We also show these natural isomorphisms satisfy the triangle and pentagon identities.

source
@[simp]
theorem CategoryTheory.whiskerLeft_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} (α : G ⟶ H) (X : C) :
(CategoryTheory.whiskerLeft F α).app X = α.app (F.obj X)
source
@[elab_without_expected_type]
def CategoryTheory.whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} (α : G ⟶ H) :
CategoryTheory.Functor.comp F G ⟶ CategoryTheory.Functor.comp F H

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

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

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

    Instances For
      source
      @[simp]
      theorem CategoryTheory.whiskeringLeft_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) :
      ((CategoryTheory.whiskeringLeft C D E).obj F).obj G = CategoryTheory.Functor.comp F G
      source
      @[simp]
      theorem CategoryTheory.whiskeringLeft_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :
      ∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (H : CategoryTheory.Functor D E) (c : C), (((CategoryTheory.whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c)
      source
      @[simp]
      theorem CategoryTheory.whiskeringLeft_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) :
      ∀ {X Y : CategoryTheory.Functor D E} (α : X ⟶ Y), ((CategoryTheory.whiskeringLeft C D E).obj F).map α = CategoryTheory.whiskerLeft F α
      source
      def CategoryTheory.whiskeringLeft (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :
      CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.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 α.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.whiskeringRight_obj_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) :
        ∀ {X Y : CategoryTheory.Functor C D} (α : X ⟶ Y), ((CategoryTheory.whiskeringRight C D E).obj H).map α = CategoryTheory.whiskerRight α H
        source
        @[simp]
        theorem CategoryTheory.whiskeringRight_map_app_app (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :
        ∀ {X Y : CategoryTheory.Functor D E} (τ : X ⟶ Y) (F : CategoryTheory.Functor C D) (c : C), (((CategoryTheory.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)
        source
        @[simp]
        theorem CategoryTheory.whiskeringRight_obj_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E) (F : CategoryTheory.Functor C D) :
        ((CategoryTheory.whiskeringRight C D E).obj H).obj F = CategoryTheory.Functor.comp F H
        source
        def CategoryTheory.whiskeringRight (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (E : Type u₃) [CategoryTheory.Category.{v₃, u₃} E] :
        CategoryTheory.Functor (CategoryTheory.Functor D E) (CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.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.

        Instances For
          source
          instance CategoryTheory.faithful_whiskeringRight_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor D E} [CategoryTheory.Faithful F] :
          CategoryTheory.Faithful ((CategoryTheory.whiskeringRight C D E).obj F)
          source
          @[simp]
          theorem CategoryTheory.whiskerLeft_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} :
          CategoryTheory.whiskerLeft F (CategoryTheory.NatTrans.id G) = CategoryTheory.NatTrans.id (CategoryTheory.Functor.comp F G)
          source
          @[simp]
          theorem CategoryTheory.whiskerLeft_id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} :
          CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.comp F G)
          source
          @[simp]
          theorem CategoryTheory.whiskerRight_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} (F : CategoryTheory.Functor D E) :
          CategoryTheory.whiskerRight (CategoryTheory.NatTrans.id G) F = CategoryTheory.NatTrans.id (CategoryTheory.Functor.comp G F)
          source
          @[simp]
          theorem CategoryTheory.whiskerRight_id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} (F : CategoryTheory.Functor D E) :
          CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.id G) F = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.comp G F)
          source
          @[simp]
          theorem CategoryTheory.whiskerLeft_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} {K : CategoryTheory.Functor D E} (α : G ⟶ H) (β : H ⟶ K) :
          CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F α) (CategoryTheory.whiskerLeft F β)
          source
          @[simp]
          theorem CategoryTheory.whiskerRight_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} {K : CategoryTheory.Functor C D} (α : G ⟶ H) (β : H ⟶ K) (F : CategoryTheory.Functor D E) :
          CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α F) (CategoryTheory.whiskerRight β F)
          source
          def CategoryTheory.isoWhiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} (α : G ≅ H) :
          CategoryTheory.Functor.comp F G ≅ CategoryTheory.Functor.comp F H

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

          Instances For
            source
            @[simp]
            theorem CategoryTheory.isoWhiskerLeft_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} (α : G ≅ H) :
            (CategoryTheory.isoWhiskerLeft F α).hom = CategoryTheory.whiskerLeft F α.hom
            source
            @[simp]
            theorem CategoryTheory.isoWhiskerLeft_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} (α : G ≅ H) :
            (CategoryTheory.isoWhiskerLeft F α).inv = CategoryTheory.whiskerLeft F α.inv
            source
            def CategoryTheory.isoWhiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : G ≅ H) (F : CategoryTheory.Functor D E) :
            CategoryTheory.Functor.comp G F ≅ CategoryTheory.Functor.comp H F

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

            Instances For
              source
              @[simp]
              theorem CategoryTheory.isoWhiskerRight_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : G ≅ H) (F : CategoryTheory.Functor D E) :
              (CategoryTheory.isoWhiskerRight α F).hom = CategoryTheory.whiskerRight α.hom F
              source
              @[simp]
              theorem CategoryTheory.isoWhiskerRight_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : G ≅ H) (F : CategoryTheory.Functor D E) :
              (CategoryTheory.isoWhiskerRight α F).inv = CategoryTheory.whiskerRight α.inv F
              source
              instance CategoryTheory.isIso_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor D E} (α : G ⟶ H) [CategoryTheory.IsIso α] :
              CategoryTheory.IsIso (CategoryTheory.whiskerLeft F α)
              source
              instance CategoryTheory.isIso_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : G ⟶ H) (F : CategoryTheory.Functor D E) [CategoryTheory.IsIso α] :
              CategoryTheory.IsIso (CategoryTheory.whiskerRight α F)
              source
              @[simp]
              theorem CategoryTheory.whiskerLeft_twice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D) {H : CategoryTheory.Functor D E} {K : CategoryTheory.Functor D E} (α : H ⟶ K) :
              CategoryTheory.whiskerLeft F (CategoryTheory.whiskerLeft G α) = CategoryTheory.whiskerLeft (CategoryTheory.Functor.comp F G) α
              source
              @[simp]
              theorem CategoryTheory.whiskerRight_twice {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] {H : CategoryTheory.Functor B C} {K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (α : H ⟶ K) :
              CategoryTheory.whiskerRight (CategoryTheory.whiskerRight α F) G = CategoryTheory.whiskerRight α (CategoryTheory.Functor.comp F G)
              source
              theorem CategoryTheory.whiskerRight_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄} [CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C) {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : G ⟶ H) (K : CategoryTheory.Functor D E) :
              CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft F α) K = CategoryTheory.whiskerLeft F (CategoryTheory.whiskerRight α K)
              source
              @[simp]
              theorem CategoryTheory.Functor.leftUnitor_hom_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) :
              (CategoryTheory.Functor.leftUnitor F).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
              source
              @[simp]
              theorem CategoryTheory.Functor.leftUnitor_inv_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) :
              (CategoryTheory.Functor.leftUnitor F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
              source
              def CategoryTheory.Functor.leftUnitor {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) :
              CategoryTheory.Functor.comp (CategoryTheory.Functor.id A) F ≅ F

              The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F.

              Instances For
                source
                @[simp]
                theorem CategoryTheory.Functor.rightUnitor_inv_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) :
                (CategoryTheory.Functor.rightUnitor F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
                source
                @[simp]
                theorem CategoryTheory.Functor.rightUnitor_hom_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) (X : A) :
                (CategoryTheory.Functor.rightUnitor F).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
                source
                def CategoryTheory.Functor.rightUnitor {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (F : CategoryTheory.Functor A B) :
                CategoryTheory.Functor.comp F (CategoryTheory.Functor.id B) ≅ F

                The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F.

                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.associator_inv_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) :
                  ∀ (x : A), (CategoryTheory.Functor.associator F G H).inv.app x = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp G H)).obj x)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.associator_hom_app {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) :
                  ∀ (x : A), (CategoryTheory.Functor.associator F G H).hom.app x = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F G) H).obj x)
                  source
                  def CategoryTheory.Functor.associator {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) :
                  CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F G) H ≅ CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp G H)

                  The associator for functors, a natural isomorphism ((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H)).

                  (In fact, iso.refl _ will work here, but it tends to make Lean slow later, and it's usually best to insert explicit associators.)

                  Instances For
                    source
                    theorem CategoryTheory.Functor.assoc {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) :
                    CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F G) H = CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp G H)
                    source
                    theorem CategoryTheory.Functor.triangle {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator F (CategoryTheory.Functor.id B) G).hom (CategoryTheory.whiskerLeft F (CategoryTheory.Functor.leftUnitor G).hom) = CategoryTheory.whiskerRight (CategoryTheory.Functor.rightUnitor F).hom G
                    source
                    theorem CategoryTheory.Functor.pentagon {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D) (K : CategoryTheory.Functor D E) :
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.Functor.associator F G H).hom K) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator F (CategoryTheory.Functor.comp G H) K).hom (CategoryTheory.whiskerLeft F (CategoryTheory.Functor.associator G H K).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.associator (CategoryTheory.Functor.comp F G) H K).hom (CategoryTheory.Functor.associator F G (CategoryTheory.Functor.comp H K)).hom