∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {X Y : AlgebraicGeometry.SheafedSpace C}
  (e : X.toPresheafedSpace ≅ Y.toPresheafedSpace),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.InducedCategory.homMk e.hom)
      (CategoryTheory.InducedCategory.homMk e.inv) =
    CategoryTheory.CategoryStruct.id X