∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α)
  (i j :
    { J := J, U := fun i => (TopologicalSpace.Opens.toTopCat { carrier := α, str := inst }).obj (U i),
        V := fun x j => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j),
        t := fun i j => TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }, V_id := ⋯, t_id := ⋯,
        t_inter := ⋯, cocycle := ⋯ }.J),
  (TopCat.GlueData.ofOpenSubsets U).f i j = ((TopologicalSpace.Opens.map (U i).inclusion').obj (U j)).inclusion'