∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} {f g : X ⟶ Y} {P : C} {ι ι' : P ⟶ X}
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g)
  (w' : CategoryTheory.CategoryStruct.comp ι' f = CategoryTheory.CategoryStruct.comp ι' g),
  ι = ι' →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fork.ofι ι w).pt).hom
        (CategoryTheory.Limits.Fork.ofι ι' w').ι =
      (CategoryTheory.Limits.Fork.ofι ι w).ι