∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData' C) (i j k : self.J)
  (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k),
  CategoryTheory.CategoryStruct.comp (self.t' i j k hij hik hjk)
      (CategoryTheory.Limits.pullback.snd (self.f j k hjk) (self.f j i ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (self.f i j hij) (self.f i k hik))
      (self.t i j hij)