{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              {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_13, u_13} E} →
                            {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₃} →
                                        {F :
                                            CategoryTheory.Functor C₁
                                              (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))} →
                                          {F' :
                                              CategoryTheory.Functor D₁
                                                (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))} →
                                            CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F' → ℕ