∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {P : CategoryTheory.ObjectProperty C} {J : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} J] {X : C} (p : P.LimitOfShape J X) {X_1 Y : J} (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.mk (p.π.app X_1)).hom
      (P.ι.map (CategoryTheory.ObjectProperty.homMk (p.diag.map f))) =
    (CategoryTheory.StructuredArrow.mk (p.π.app Y)).hom