∀ {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} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {C : Type u_4} [inst_5 : CategoryTheory.Category.{v_4, u_4} C]
  (F : CategoryTheory.Functor C (CategoryTheory.Comma L R)) (hP : ∀ (X : C), P (F.obj X).hom)
  (hQ : ∀ {X Y : C} (f : X ⟶ Y), Q (F.map f).left) (hW : ∀ {X Y : C} (f : X ⟶ Y), W (F.map f).right) (X : C),
  ((CategoryTheory.MorphismProperty.Comma.lift F hP hQ hW).obj X).toComma = F.obj X