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>=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(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 ell(alpha), alpha<kappa, must lie in V_kappa. Lambda=kappa and x=empty are included. This definition asserts no existence of such ell; that is the separate existence theorem.