{P : Sort u} →
  {A : Type u_1} →
    {G : Type u_2} →
      {V : Type u_3} →
        {W : Type u_4} →
          {inst : CommRing A} →
            {inst_1 : Monoid G} →
              {inst_2 : AddCommMonoid V} →
                {inst_3 : AddCommMonoid W} →
                  {inst_4 : Module A V} →
                    {inst_5 : Module A W} →
                      {ρ : Representation A G V} →
                        {σ : Representation A G W} →
                          {t : ρ.IntertwiningMap σ} →
                            {A' : Type u_1} →
                              {G' : Type u_2} →
                                {V' : Type u_3} →
                                  {W' : Type u_4} →
                                    {inst' : CommRing A'} →
                                      {inst'_1 : Monoid G'} →
                                        {inst'_2 : AddCommMonoid V'} →
                                          {inst'_3 : AddCommMonoid W'} →
                                            {inst'_4 : Module A' V'} →
                                              {inst'_5 : Module A' W'} →
                                                {ρ' : Representation A' G' V'} →
                                                  {σ' : Representation A' G' W'} →
                                                    {t' : ρ'.IntertwiningMap σ'} →
                                                      A = A' →
                                                        G = G' →
                                                          V = V' →
                                                            W = W' →
                                                              inst ≍ inst' →
                                                                inst_1 ≍ inst'_1 →
                                                                  inst_2 ≍ inst'_2 →
                                                                    inst_3 ≍ inst'_3 →
                                                                      inst_4 ≍ inst'_4 →
                                                                        inst_5 ≍ inst'_5 →
                                                                          ρ ≍ ρ' →
                                                                            σ ≍ σ' →
                                                                              t ≍ t' →
                                                                                Representation.IntertwiningMap.noConfusionType
                                                                                  P t t'