Sort u →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} A] →
      {B : Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
          {T : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
              {L : CategoryTheory.Functor A T} →
                {R : CategoryTheory.Functor B T} →
                  {P : CategoryTheory.MorphismProperty T} →
                    {Q : CategoryTheory.MorphismProperty A} →
                      {W : CategoryTheory.MorphismProperty B} →
                        {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} →
                          X.Hom Y →
                            {A' : Type u_1} →
                              [inst' : CategoryTheory.Category.{v_1, u_1} A'] →
                                {B' : Type u_2} →
                                  [inst'_1 : CategoryTheory.Category.{v_2, u_2} B'] →
                                    {T' : Type u_3} →
                                      [inst'_2 : CategoryTheory.Category.{v_3, u_3} T'] →
                                        {L' : CategoryTheory.Functor A' T'} →
                                          {R' : CategoryTheory.Functor B' T'} →
                                            {P' : CategoryTheory.MorphismProperty T'} →
                                              {Q' : CategoryTheory.MorphismProperty A'} →
                                                {W' : CategoryTheory.MorphismProperty B'} →
                                                  {X' Y' : CategoryTheory.MorphismProperty.Comma L' R' P' Q' W'} →
                                                    X'.Hom Y' → Sort u