∀ {J : Type v₁} {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C]
  (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) {j : CategoryTheory.Discrete J} (f : j ⟶ j),
  F.map f = CategoryTheory.CategoryStruct.id (F.obj j)