∀ {D : Type u_1} {I : Type u_2} {J : Type u_3} [inst : Zero I] (p : I × J → J),
  (∀ (j : J), p (0, j) = j) →
    ∀ (Y : CategoryTheory.GradedObject J D) (j : J) (a : I × J), p a = j → a.1 = 0 → Y a.2 = Y j