∀ {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} [inst_1 : X.HasMap p] {A : C} {j : J} {f g : X.mapObj p j ⟶ A},
  f = g ↔
    ∀ (i : I) (hij : p i = j),
      CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f =
        CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g