∀ (X : TopCat) {X_1 Y Z : TopologicalSpace.Opens ↑X} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
  TopCat.ofHom { toFun := fun x => ⟨↑x, ⋯⟩, continuous_toFun := ⋯ } =
    CategoryTheory.CategoryStruct.comp (TopCat.ofHom { toFun := fun x => ⟨↑x, ⋯⟩, continuous_toFun := ⋯ })
      (TopCat.ofHom { toFun := fun x => ⟨↑x, ⋯⟩, continuous_toFun := ⋯ })