-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- The associator isomorphism obtained by localization.  -/
CategoryTheory.Localization.associator : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₁₂ : Type u_4} →
        {C₂₃ : Type u_5} →
          {D₁ : Type u_6} →
            {D₂ : Type u_7} →
              {D₃ : Type u_8} →
                {D₁₂ : Type u_9} →
                  {D₂₃ : Type u_10} →
                    {C : Type u_11} →
                      {D : Type u_12} →
                        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
                          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                              [inst_3 : CategoryTheory.Category.{v_4, u_6} D₁] →
                                [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                                  [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                                    [inst_6 : CategoryTheory.Category.{v_7, u_4} C₁₂] →
                                      [inst_7 : CategoryTheory.Category.{v_8, u_5} C₂₃] →
                                        [inst_8 : CategoryTheory.Category.{v_9, u_9} D₁₂] →
                                          [inst_9 : CategoryTheory.Category.{v_10, u_10} D₂₃] →
                                            [inst_10 : CategoryTheory.Category.{v_11, u_11} C] →
                                              [inst_11 : CategoryTheory.Category.{v_12, u_12} D] →
                                                (L₁ : CategoryTheory.Functor C₁ D₁) →
                                                  (L₂ : CategoryTheory.Functor C₂ D₂) →
                                                    (L₃ : CategoryTheory.Functor C₃ D₃) →
                                                      (L₁₂ : CategoryTheory.Functor C₁₂ D₁₂) →
                                                        (L₂₃ : CategoryTheory.Functor C₂₃ D₂₃) →
                                                          (L : CategoryTheory.Functor C D) →
                                                            (W₁ : CategoryTheory.MorphismProperty C₁) →
                                                              (W₂ : CategoryTheory.MorphismProperty C₂) →
                                                                (W₃ : CategoryTheory.MorphismProperty C₃) →
                                                                  (W₁₂ : CategoryTheory.MorphismProperty C₁₂) →
                                                                    (W₂₃ : CategoryTheory.MorphismProperty C₂₃) →
                                                                      [W₁.ContainsIdentities] →
                                                                        [W₂.ContainsIdentities] →
                                                                          [W₃.ContainsIdentities] →
                                                                            [L₁.IsLocalization W₁] →
                                                                              [L₂.IsLocalization W₂] →
                                                                                [L₃.IsLocalization W₃] →
                                                                                  {F₁₂ :
                                                                                      CategoryTheory.Functor C₁
                                                                                        (CategoryTheory.Functor C₂
                                                                                          C₁₂)} →
                                                                                    {G :
                                                                                        CategoryTheory.Functor C₁₂
                                                                                          (CategoryTheory.Functor C₃
                                                                                            C)} →
                                                                                      {F :
                                                                                          CategoryTheory.Functor C₁
                                                                                            (CategoryTheory.Functor C₂₃
                                                                                              C)} →
                                                                                        {G₂₃ :
                                                                                            CategoryTheory.Functor C₂
                                                                                              (CategoryTheory.Functor C₃
                                                                                                C₂₃)} →
                                                                                          (CategoryTheory.bifunctorComp₁₂
                                                                                                F₁₂ G ≅
                                                                                              CategoryTheory.bifunctorComp₂₃
                                                                                                F G₂₃) →
                                                                                            (F₁₂' :
                                                                                                CategoryTheory.Functor
                                                                                                  D₁
                                                                                                  (CategoryTheory.Functor
                                                                                                    D₂ D₁₂)) →
                                                                                              (G' :
                                                                                                  CategoryTheory.Functor
                                                                                                    D₁₂
                                                                                                    (CategoryTheory.Functor
                                                                                                      D₃ D)) →
                                                                                                (F' :
                                                                                                    CategoryTheory.Functor
                                                                                                      D₁
                                                                                                      (CategoryTheory.Functor
                                                                                                        D₂₃ D)) →
                                                                                                  (G₂₃' :
                                                                                                      CategoryTheory.Functor
                                                                                                        D₂
                                                                                                        (CategoryTheory.Functor
                                                                                                          D₃ D₂₃)) →
                                                                                                    [⋯] → ⋯