∀ {X : Type u_1} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {X_1 Y : TopologicalSpace.Opens ↥U}
  (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (({ obj := fun W => CategoryTheory.Over.mk (CategoryTheory.homOfLE ⋯),
                map := fun {X_2 Y} f => CategoryTheory.Over.homMk (CategoryTheory.homOfLE ⋯) ⋯, map_id := ⋯,
                map_comp := ⋯ }.comp
            { obj := fun V => { carrier := Subtype.val ⁻¹' ↑V.left, is_open' := ⋯ },
              map := fun {X_2 Y} f => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }).map
        f)
      ((fun V => CategoryTheory.eqToIso ⋯) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun V => CategoryTheory.eqToIso ⋯) X_1).hom
      ((CategoryTheory.Functor.id (TopologicalSpace.Opens ↥U)).map f)