∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (φ : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.FreeGroupoid.map φ).obj (CategoryTheory.FreeGroupoid.mk X) = CategoryTheory.FreeGroupoid.mk (φ.obj X)