∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z X' Y' Z' : C} {f : X ⟶ Y} {g : Y ⟶ Z}
  {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'},
  X = X' →
    Y = Y' →
      Z = Z' → f ≍ f' → g ≍ g' → CategoryTheory.CategoryStruct.comp f g ≍ CategoryTheory.CategoryStruct.comp f' g'