{P : Sort u_1} →
  {R : Type u} →
    {S : Type v} →
      {ι : Type w} →
        {σ : Type t} →
          {inst : CommRing R} →
            {inst_1 : CommRing S} →
              {inst_2 : Algebra R S} →
                {t : Algebra.PreSubmersivePresentation R S ι σ} →
                  {R' : Type u} →
                    {S' : Type v} →
                      {ι' : Type w} →
                        {σ' : Type t} →
                          {inst' : CommRing R'} →
                            {inst'_1 : CommRing S'} →
                              {inst'_2 : Algebra R' S'} →
                                {t' : Algebra.PreSubmersivePresentation R' S' ι' σ'} →
                                  R = R' →
                                    S = S' →
                                      ι = ι' →
                                        σ = σ' →
                                          inst ≍ inst' →
                                            inst_1 ≍ inst'_1 →
                                              inst_2 ≍ inst'_2 →
                                                t ≍ t' → Algebra.PreSubmersivePresentation.noConfusionType P t t'