∀ (R : Type u_2) [inst : Ring R] [inst_1 : TopologicalSpace R] (X : TopModuleCat R),
  ModuleCat.ofHom ↑(TopModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id X)) =
    CategoryTheory.CategoryStruct.id (ModuleCat.of R ↑X.toModuleCat)