∀ (R : Type u_1) [inst : Ring R] [inst_1 : TopologicalSpace R],
  { obj := fun M => TopCat.of ↑M.toModuleCat,
          map := fun {X Y} φ =>
            TopCat.ofHom { toFun := ⇑(CategoryTheory.ConcreteCategory.hom φ), continuous_toFun := ⋯ },
          map_id := ⋯, map_comp := ⋯ }.comp
      (CategoryTheory.forget TopCat) =
    CategoryTheory.forget (TopModuleCat R)