∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) (j : J) (pt : C) (ι' : (i : I) → p i = j → (X i ⟶ pt)),
  CategoryTheory.GradedObject.CofanMapObjFun.mk X p j pt ι' =
    CategoryTheory.Limits.Cofan.mk pt fun x =>
      match x with
      | ⟨i, hi⟩ => ι' i hi