∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {kf : CategoryTheory.Limits.KernelFork f}
  {kf' : CategoryTheory.Limits.KernelFork f'} (hf : CategoryTheory.Limits.IsLimit kf)
  (hf' : CategoryTheory.Limits.IsLimit kf') (φ : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp (kf'.mapOfIsLimit hf φ.inv) (kf.mapOfIsLimit hf' φ.hom) =
    CategoryTheory.CategoryStruct.id kf'.pt