{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {M : Type u_3} →
                [inst_2 : AddMonoid M] →
                  [inst_3 : CategoryTheory.HasShift C₁ M] →
                    [inst_4 : CategoryTheory.HasShift C₂ M] →
                      [Φ.functor.CommShift M] →
                        {D₁ : Type u_4} →
                          {D₂ : Type u_5} →
                            [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁] →
                              [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] →
                                (L₁ : CategoryTheory.Functor C₁ D₁) →
                                  [inst_8 : L₁.IsLocalization W₁] →
                                    (L₂ : CategoryTheory.Functor C₂ D₂) →
                                      [inst_9 : CategoryTheory.HasShift D₁ M] →
                                        [inst_10 : CategoryTheory.HasShift D₂ M] →
                                          [L₁.CommShift M] →
                                            [L₂.CommShift M] →
                                              [inst_13 : L₂.IsLocalization W₂] → (Φ.localizedFunctor L₁ L₂).CommShift M