The notion of modulus of continuity is well-known from constructive mathematics, reverse mathematics, and computability theory. Intuitively, such a modulus is a function that returns the '$\delta>0$' on input an '$\epsilon>0$' and a point in the domain.
In reverse mathematics, the second-order representation of continuous functions is equivalent to the existence of a continuous modulus of continuity, as shown by Kohlenbach.
I vaguely recall there being developments of (constructive?) mathematics where one considers continuous functions that come with a continuous modulus of continuity and a continuous modulus of continuity for the latter modulus.
Can someone provide a reference for the aforementioned construct?
EDIT: following a question, here is the formal statement of the second paragraph:
For any $Y:\mathbb{N}^{\mathbb{N}}\rightarrow\mathbb{N}$, the following are equivalent:
There is a total (Kleene) associate $\alpha\in \mathbb{N}^{\mathbb{N}}$ such that $\alpha(f)=Y(f)$ for any $f\in \mathbb{N}^{\mathbb{N}}$,
There is a (second-order) RM-code $\Phi$, for which the value $\Phi(f)$ equals $Y(f)$ for any $f\in \mathbb{N}^{\mathbb{N}}$,
The functional $Y$ has a modulus of continuity.
See Section 4 in "FOUNDATIONAL AND MATHEMATICAL USES OF HIGHER TYPES" by Kohlenbach.
