∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {P : CategoryTheory.Subobject Y}
  (f : X ⟶ CategoryTheory.Subobject.underlying.obj P), P.Factors (CategoryTheory.CategoryStruct.comp f P.arrow)