Type/codomain of constant function $f(x)=5$ A function like $f(x) = 2x$ can be defined over the reals so its “type signature” or in set theory domain and codomain is $f: \mathbb{R} \rightarrow \mathbb{R}$. 
I want to define a function $f(x) = 5$ (or some other constant number) and restrict the codomain/return type to be a constant value. What is the (most restrictive) type signature of such a function? Does this require dependent types? Is it $f: \mathbb{R} \rightarrow 5$? I want to know the type signature for that specific function that returns $5$ and the more general notion of a function that returns a constant value that does not depend on the input argument. 
My motivation is that I want to be able to describe in a precise way functions that do not use/“delete” their input argument and return some other constant value. Eventually, I want to formalize this in a proof assistant. 

Define the type $\mathsf{Five}$ as the singleton type populated by the type axiom $E \vdash 5 : \mathsf{Five}$. Then the type of $f$ is $f : \mathbb{R} \rightarrow \mathsf{Five}$.
