∀ {X Y : TopCatᵒᵖ} (f : X ⟶ Y) (R : TopCommRingCat)
  (x y : Opposite.unop X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R),
  CategoryTheory.CategoryStruct.comp f.unop (x + y) =
    CategoryTheory.CategoryStruct.comp f.unop x + CategoryTheory.CategoryStruct.comp f.unop y