∀ (R : Type u_2) [inst : CommRing R] (X : CommAlgCat R),
  CommAlgCat.ofHom
      ((↑ULift.algEquiv.symm).comp ((CommAlgCat.Hom.hom (CategoryTheory.CategoryStruct.id X)).comp ↑ULift.algEquiv)) =
    CategoryTheory.CategoryStruct.id (CommAlgCat.of R (ULift.{u_3, u_1} ↑X))