∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {β : Type u_1} (X Y : CategoryTheory.GradedObject β C)
  (e : (i : β) → X i ≅ Y i),
  (CategoryTheory.CategoryStruct.comp (fun i => (e i).inv) fun i => (e i).hom) = CategoryTheory.CategoryStruct.id Y