∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {S : D} {T : CategoryTheory.Functor C D}
  {A : CategoryTheory.StructuredArrow S T} (P : CategoryTheory.Subobject A.right)
  {q : (CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj P)}
  (hq : CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom),
  CategoryTheory.Mono (CategoryTheory.StructuredArrow.homMk P.arrow hq)