∀ {C : Type u_4} [inst : CategoryTheory.Groupoid C] {D : Type u_2} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (c : C),
  φ.map (CategoryTheory.CategoryStruct.id c) = CategoryTheory.CategoryStruct.id (φ.obj c)