∀ {X Y Z : CommRingCatᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
  AlgebraicGeometry.Spec.locallyRingedSpaceMap (CategoryTheory.CategoryStruct.comp f g).unop =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.locallyRingedSpaceMap f.unop)
      (AlgebraicGeometry.Spec.locallyRingedSpaceMap g.unop)