There are still some loose threads which have not been entirely sewn up. Following up on YCor's question on definability constraints: the collection of semi-algebraic sets can also be defined so that by definition it is closed under taking images along projection maps (and then Tarski-Seidenberg assures us we could do with less). Should I assume you don't allow that, i.e., "definability" here excludes existential quantification? Also, would you allow the modulus map to be seen as a function $\mathbb{C} \to \mathbb{C}$, i.e., as the interpretation of an unary function symbol in the signature?

Notably Barr. (I'm not aware that everyone else is or was adamant about it, and I lived there for six months.) Added later: Joyal says "monad"; I've never heard him say "triple".

Surely a kind of back-formation from monoid? Coupled perhaps with the love of purloining terms from philosophy. I don't know that it needed more than one event, namely the recognition that a monad is a monoid in a category of endofunctors, like his book says.

Rolling back from a pointless edit.

I took the liberty of adding your answer as an edit, and while I was at it, I also fixed up the English a little (hope you don't mind).

This looks like it has big list potential, so I'm making it CW.

I'm copying @MikeShulman to alert him to your question (Oren), as he would have a much better chance of saying something meaningful.

@OrenBen-Bassat Sadly, my feeling for higher topos theory is not all that it could or should be. However, ...

@FedorPetrov Could be; I was just wondering if anyone had information on that, not that I positively suspect it is a current contest problem. Incidentally, do you happen to know what the famous inequality refers to?

Tarski's method gives a way of translating a problem in Elementary Plane Geometry (in the technical sense made precise by his axioms for geometry) into a problem about real-closed fields, and the first-order theory of real-closed field is decidable, using the Tarski-Seidenberg theorem which allows for quantifier elimination. (Presumably the statements you have in mind about properties picking out one of the two points of circle intersections are statements expressible in terms of field ordering.) But algorithms for eliminating quantifiers have complexity unbounded by stacks of exponentials.