Theorems · Definition · category theory

CategoryTheory.Functor.associator

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                (F : CategoryTheory.Functor C D) →
                  (G : CategoryTheory.Functor D E) →
                    (H : CategoryTheory.Functor E E') → (F.comp G).comp H ≅ F.comp (G.comp 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.)

Defined in

Mathlib.CategoryTheory.Functor.Category

Cited by

276 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 109 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category