∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b)
  {j j' : β} (w : j = j'),
  CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.eqToHom ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j')