Oh sorry! I'm editing once more.

Cool! Can you provide any conventional reference where it is actually possible to find the same kind of proof? That of Herman (M.R. Herman (1979), Sur la conjugaison différentiable des difféomorphismes du cercle à des rotations, Publ. Math. IHES, Vol. 49, pp. 5–234) looks different.

Thank you, Denis, this definitely fills the bill. Yet, unless I'm misunderstanding your thoughts, I can't figure out by myself how to use Fekete's result to prove the existence of the relevant limit in the definition of the rotation number. How do you show that, given $f: \mathbb{S}^1 \to \mathbb{S}^1$ an orientation-preserving homeomorphism of the circle, $F: \mathbb{R} \to \mathbb{R}$ a continuous lift of $f$ and $x$ an arbitrary point in $\mathbb{S}^1$, it is $F^{m+n}(x) \bmod 1 \le F^{m}(x) \bmod 1 + F^{n}(x) \bmod 1$ for all $m, n \in \mathbb{N}$?

Let me try and guess that "over the reals" means that the carrier of the structure is the reals. On another hand, I don't understand why the OP speaks of an ordered group but specifies what looks like the signature of an ordered monoid.

Thanks you all. In one way or another, your comments have unhinged a little door in my mind. And yes, I'm definitely reconsidering the option of generalized elements (though not in its full generality). In any event, I'm still interested in a historical overview of the notion itself of point in category theory as well as in a list, as complete as possible, of its most significant embodiments. I see that it may be an overwhelming request but asking is not a sin.

...on any result which is local to the (classical) theory of either metric or normed (vector) spaces?

@quid. I don't think so, since a structure, as you can read in the OP (and I've been repeating since the very beginning), must be intended as a "model of a finitary first-order theory interpreted over $\bf Set$ or another category $\bf C$ with appropriate properties." Though we can embed a metric space into a normed one (by the Kuratowski embedding theorem), the embedding is not sending a metric space into a $\bf Set$-model of the first-order theory of real normed spaces. Isn't clear that any possible unification of the two concepts (that of metric and the one of norm) cannot depend... (tbc)

Moreover, I disagree with the fact that "norms" have to be convex functions. Yes, of course, they are convex if you focus on the case of normed (vector) spaces. But convexity doesn't happen to be a property, e.g., of group norms and ring valuations. @Yemon. Why do we look for unifying views in mathematics? And, above all, what is NCG?!?

@Suvrit. The question is: Do you know of any previous attempt to put metric spaces and normed structures within one same abstract framework, in such a way that the former and the latter are definitely recovered as specializations of one same abstract notion of "structure"? What I mean by "structure" is explained at the end of the OP: The term "structure" must be formally intended as "model of a finitary first-order theory (in one or many sorts) interpreted over Set or another category C with some appropriate properties" [...].