Let $\exp$ be the D1932: Standard natural real exponential function.
The standard natural hyperbolic cosine function is the D4364: Real function \begin{equation} \cosh : \mathbb{R} \to \mathbb{R}, \quad \cosh(x) = \frac{1}{2} (\exp(x) + \exp(-x)) \end{equation}