Let $T$ be the complete hierarchy of functions over $\mathbb{N}$. That is: $T$ = $\bigcup T_{\tau}$ for all simple types $\tau$ built up from the basic type $\mathbb{N}$, with $T_{\mathbb{N}} = \mathbb{N}$ and $T_{\alpha→\beta} = {T_\beta}^{T_\alpha}$. For a given signature $\Sigma$ consisting of some members of $T$, there is an obvious way of interpreting the closed terms of type $\tau$ in a simply typed $\lambda$-language $\mathcal{L}_\Sigma$ with constants from $\Sigma$ as denoting functions in $T_\tau$. Let ${T^\Sigma}$ contain just those members of $T$ that are denoted by closed terms in $\mathcal{L}_\Sigma$. Say that $T^\Sigma$ is functional just in case, for any distinct $f, g ∈ {T^\Sigma}_{\alpha→\beta}$, there is some $x ∈ {T^\Sigma}_\alpha$ such that $f(x) \ne g(x)$.
Specific question: let $\Sigma$ consist in all members of $\mathbb{N}$ (of type $\mathbb{N}$) together with the addition function (of type $\mathbb{N}→\mathbb{N}→\mathbb{N}$). Is this $T^\Sigma$ functional?
More general question: is there any useful general condition on $\Sigma$ that is sufficient for $T^\Sigma$ to be functional?
