∀ (R : CommRingCatᵒᵖ),
  AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.id R).unop =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec.locallyRingedSpaceObj (Opposite.unop R))