Full-completeness conjecture for universal operations on grounds

Let $\Lambda$ be over the base structure $\mathfrak{B}_1$, and let $den^*_1$ be a denotation relative to $\Lambda$ such that, for some operational symbol $\phi$ of $\Lambda$, $den^*_1(\phi)$ is a universal operation on grounds $f$. Full-completeness conjecture. There should exist a denotation $den^*_2$ relative to $\texttt{Gen}$ over $\mathfrak{B}_1$ and operational symbols $\phi_1,\ldots,\phi_n$ of $\texttt{Gen}$ such that a universal operation on grounds $h$, composed of $den^*_2(\phi_1),\ldots,den^*_2(\phi_n)$, agrees extensionally with $den^*_1(\phi)$ on every $\mathfrak{B}_2$: if $g_1$ is the ground on $\mathfrak{B}_2$ satisfying $den^*_1(\phi)\approx_{\mathfrak{B}_1,\mathfrak{B}_2}g_1$ and $g_2$ is the ground on $\mathfrak{B}_2$ satisfying $h\approx_{\mathfrak{B}_1,\mathfrak{B}_2}g_2$, then $g_1\equiv_{\mathfrak{B}_2}g_2$. This is stronger than Prawitz's conjecture: it asks that every universal operation inhabiting the relevant type be extensionally represented by the denotation of a term of $\texttt{Gen}$, rather than merely that the type be derivable in intuitionistic logic.