{P : Sort u} →
  {M : Type u_1} →
    {inst : CommMonoid M} →
      {S : Submonoid M} →
        {N : Type u_2} →
          {inst_1 : CommMonoid N} →
            {t : S.LocalizationMap N} →
              {M' : Type u_1} →
                {inst' : CommMonoid M'} →
                  {S' : Submonoid M'} →
                    {N' : Type u_2} →
                      {inst'_1 : CommMonoid N'} →
                        {t' : S'.LocalizationMap N'} →
                          M = M' →
                            inst ≍ inst' →
                              S ≍ S' →
                                N = N' → inst_1 ≍ inst'_1 → t ≍ t' → Submonoid.LocalizationMap.noConfusionType P t t'