{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) →
                      [SizeOf A] →
                        [SizeOf B] →
                          [SizeOf T] →
                            [⦃X Y : T⦄ → (x : X ⟶ Y) → SizeOf (P x)] →
                              [⦃X Y : A⦄ → (x : X ⟶ Y) → SizeOf (Q x)] →
                                [⦃X Y : B⦄ → (x : X ⟶ Y) → SizeOf (W x)] →
                                  SizeOf (CategoryTheory.MorphismProperty.Comma L R P Q W)