∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j : self.J)
  (hij : i ≠ j),
  CategoryTheory.CategoryStruct.comp (self.t i j hij) (self.t j i ⋯) = CategoryTheory.CategoryStruct.id (self.V i j hij)