The absolute value function is the D4367: Unsigned real function \begin{equation} \mathbb{R} \to [0, \infty), \quad x \mapsto x I_{[0, \infty)}(x) - x I_{(- \infty, 0)}(x) \end{equation}