Suppose that $M$ is a full model of the simply typed lambda calculus. Suppose each base type is infinite.
Now suppose that $f$ and $g$ are two functions in $M$ (not necessarily in the same domain) that are not definable by any pure term, and that $\alpha$ is a pure term of the $\lambda$-calculus such that: $$M(\alpha) g = f $$
My question is: when is it possible to find a pure term $\beta$ such that $$g=M(\beta)f$$
Are there easy to state necessary or sufficient conditions? I have been unable to find counterexamples when gs type complexity is higher than fs, so maybe that is a sufficient condition?
A couple of examples:
if $f$ is the converse of $g$: $$f=M(\lambda xyz. xzy)g$$ then we can find such a $\beta$ -- in this case, letting it also be $\lambda xyz. xzy$.
Similarly If $f$ is application to $a$: $$f = M(\lambda xy.yx)a$$ then $a$ is $f$ applied to $\lambda x.x$: $$a = M(\lambda y.y(\lambda x.x))f$$
Lastly, if $x$ is a variable in some base type and $f=M(\lambda xy.x)a$, then I don't think there is any pure term such that $a=M(\beta)f$.