∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] (F : CategoryTheory.Functor C TopCat) (Y : Type u_3)
  [inst_1 : TopologicalSpace Y] (X : Cᵒᵖ),
  (fun g => g.comp (TopCat.Hom.hom (F.map (CategoryTheory.CategoryStruct.id X).unop))) =
    CategoryTheory.CategoryStruct.id C(↑(F.obj (Opposite.unop X)), Y)