∀ (D : TopCat.GlueData) (i j : D.J) (U : Set ↑(D.U i)),
  ⇑(CategoryTheory.ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(CategoryTheory.ConcreteCategory.hom (D.ι i)) '' U) =
    ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i))) ''
      (⇑(CategoryTheory.ConcreteCategory.hom (D.f i j)) ⁻¹' U)