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