∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : CategoryTheory.CatCenter C) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (z.app Y) = CategoryTheory.CategoryStruct.comp (z.app X) f