Laver anticipation functions

Work in ZFC, with The Axiom of Choice, and suppose $\kappa$ is supercompact in the sense of Fine measures, strong compactness and supercompactness. A Laver anticipation function is a set function $\mathrm{\ell }:\kappa \to V_{\kappa }$ such that for every set $x$ and every cardinal $\lambda \ge \kappa$ there is a supercompactness embedding $j:V\to M$ with

$\mathrm{crit}(j)=\kappa ,j(\kappa )>\lambda ,{}^{\lambda }M\subseteq M,j(\mathrm{\ell })(\kappa )=x\mathrm{.}$

Here the sequence-closure condition and embeddings have the precise definable-class, set-restriction and formula-by-formula meaning in Supercompactness and closed elementary embeddings. In particular no uniform truth predicate for $V$ or unrestricted class quantifier is introduced: the witness is supplied by a definition with set parameters, and its elementarity is verified as a schema. Since $j(\mathrm{\ell })$ is a function with domain $j(\kappa )$ and $\kappa <j(\kappa )$, its value at $\kappa$ is well-defined. The anticipated $x$ can have rank at least $\kappa$; only the original values $\mathrm{\ell }(\alpha )$, $\alpha <\kappa$, must lie in $V_{\kappa }$. $\lambda =\kappa$ and $x=\mathrm{\varnothing }$ are included. This definition asserts no existence of such $\mathrm{\ell }$; that is the separate existence theorem.