Sort u →
  {C₁ : Type u_1} →
    {C₂ : Type u_2} →
      {D₁ : Type u_3} →
        {D₂ : Type u_4} →
          {E : Type u_5} →
            [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} D₁] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                      {L₁ : CategoryTheory.Functor C₁ D₁} →
                        {L₂ : CategoryTheory.Functor C₂ D₂} →
                          {W₁ : CategoryTheory.MorphismProperty C₁} →
                            {W₂ : CategoryTheory.MorphismProperty C₂} →
                              {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)} →
                                {F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)} →
                                  CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F' →
                                    {C₁' : Type u_1} →
                                      {C₂' : Type u_2} →
                                        {D₁' : Type u_3} →
                                          {D₂' : Type u_4} →
                                            {E' : Type u_5} →
                                              [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} D₁'] →
                                                    [inst'_3 : CategoryTheory.Category.{v_4, u_4} D₂'] →
                                                      [inst'_4 : CategoryTheory.Category.{v_5, u_5} E'] →
                                                        {L₁' : CategoryTheory.Functor C₁' D₁'} →
                                                          {L₂' : CategoryTheory.Functor C₂' D₂'} →
                                                            {W₁' : CategoryTheory.MorphismProperty C₁'} →
                                                              {W₂' : CategoryTheory.MorphismProperty C₂'} →
                                                                {F' :
                                                                    CategoryTheory.Functor C₁'
                                                                      (CategoryTheory.Functor C₂' E')} →
                                                                  {F'' :
                                                                      CategoryTheory.Functor D₁'
                                                                        (CategoryTheory.Functor D₂' E')} →
                                                                    CategoryTheory.Localization.Lifting₂ L₁' L₂' W₁' W₂'
                                                                        F' F'' →
                                                                      Sort u