∀ {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) (U : TopologicalSpace.Opens ↑Y)
  (q : (CategoryTheory.ConcreteCategory.hom f) x ∈ U),
  (TopologicalSpace.OpenNhds.map f x).obj ⟨U, q⟩ = ⟨(TopologicalSpace.Opens.map f).obj U, q⟩