{P : Sort u} →
  {k : Type u_1} →
    {V : Type u_2} →
      {P_1 : Type u_5} →
        {inst : Ring k} →
          {inst_1 : AddCommGroup V} →
            {inst_2 : Module k V} →
              {inst_3 : AddTorsor V P_1} →
                {n : ℕ} →
                  {t : Affine.Simplex k P_1 n} →
                    {k' : Type u_1} →
                      {V' : Type u_2} →
                        {P' : Type u_5} →
                          {inst' : Ring k'} →
                            {inst'_1 : AddCommGroup V'} →
                              {inst'_2 : Module k' V'} →
                                {inst'_3 : AddTorsor V' P'} →
                                  {n' : ℕ} →
                                    {t' : Affine.Simplex k' P' n'} →
                                      k = k' →
                                        V = V' →
                                          P_1 = P' →
                                            inst ≍ inst' →
                                              inst_1 ≍ inst'_1 →
                                                inst_2 ≍ inst'_2 →
                                                  inst_3 ≍ inst'_3 →
                                                    n = n' → t ≍ t' → Affine.Simplex.noConfusionType P t t'