∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} (f : A.left ⟶ B.left) (hf : Q f)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f) B.hom = A.hom)
      CategoryTheory.MorphismProperty.CostructuredArrow.homMk._auto_1),
  (CategoryTheory.MorphismProperty.CostructuredArrow.homMk f hf w).left = f