is there anything nontrivial here? I guess we are now allowed to write "topological" before anything in FOL and have it make sense
similarly things with some kind of symmetry

I don't know enough category theory and am a bear of v little brain

(ed: finite products)

ok i guess we may need coproducts as well to express disjunctions
"either x has a multiplicative inverse or x is 0"
not sure the reals are a "topological field" in this sense though
or we have to settle for a rather more resticted set of FOL objects

@alexthecamel Yep. One caveat is that it often has to be constructive first order logic rather than classical first order logic, because the law of excluded middle fails in many useful categories. E.g. law of excluded middle can be used to define discontinuous functions, and so doesn't hold topologically.

@alexthecamel First order logic structures in general requires toposes, not just products. However, it is true for any algebraic structure (monoids, groups, rings, ... BUT NOT fields because fields aren't a true algebraic structure due to having a != 0 condition on division).