{P : Sort u} →
  {C₁ : Type u_1} →
    {C₂ : Type u_2} →
      {C₃ : Type u_3} →
        {C₄ : Type u_4} →
          {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
            {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} →
              {inst_2 : CategoryTheory.Category.{v_3, u_3} C₃} →
                {inst_3 : CategoryTheory.Category.{v_4, u_4} C₄} →
                  {T : CategoryTheory.Functor C₁ C₂} →
                    {L : CategoryTheory.Functor C₁ C₃} →
                      {R : CategoryTheory.Functor C₂ C₄} →
                        {B : CategoryTheory.Functor C₃ C₄} →
                          {t : CategoryTheory.CatCommSq T L R B} →
                            {C₁' : Type u_1} →
                              {C₂' : Type u_2} →
                                {C₃' : Type u_3} →
                                  {C₄' : Type u_4} →
                                    {inst' : CategoryTheory.Category.{v_1, u_1} C₁'} →
                                      {inst'_1 : CategoryTheory.Category.{v_2, u_2} C₂'} →
                                        {inst'_2 : CategoryTheory.Category.{v_3, u_3} C₃'} →
                                          {inst'_3 : CategoryTheory.Category.{v_4, u_4} C₄'} →
                                            {T' : CategoryTheory.Functor C₁' C₂'} →
                                              {L' : CategoryTheory.Functor C₁' C₃'} →
                                                {R' : CategoryTheory.Functor C₂' C₄'} →
                                                  {B' : CategoryTheory.Functor C₃' C₄'} →
                                                    {t' : CategoryTheory.CatCommSq T' L' R' B'} →
                                                      C₁ = C₁' →
                                                        C₂ = C₂' →
                                                          C₃ = C₃' →
                                                            C₄ = C₄' →
                                                              inst ≍ inst' →
                                                                inst_1 ≍ inst'_1 →
                                                                  inst_2 ≍ inst'_2 →
                                                                    inst_3 ≍ inst'_3 →
                                                                      T ≍ T' →
                                                                        L ≍ L' →
                                                                          R ≍ R' →
                                                                            B ≍ B' →
                                                                              t ≍ t' →
                                                                                CategoryTheory.CatCommSq.noConfusionType
                                                                                  P t t'