{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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'} →
                  CategoryTheory.Limits.IsLimit kf →
                    CategoryTheory.Limits.IsLimit kf' →
                      (CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f') → (kf.pt ≅ kf'.pt)