A question regarding models of $ZF+I_0$ [Revised] In his answer to user42090's mathoverflow question"Minimal Generalized Contnuum Hypothesis & Axiom of Choice", Prof. Hamkins writes:
"...one can build the analogue of the symmetric models for $\lnot$$AC$ above any cardinal, while preserving $GCH$ below..."
Are there any examples of such models in the literature which also satisfy the large cardinal axiom $I_0$ (which builds the symmetric model satisfying $\lnot$$AC$  above the '$I_0$ cardinals') , and how are these models constructed by forcing?
Also, if such models exist, can they serve as a 'laboratory' to study the behavior of $ZF$ beyond the '$AC$ barrier'?
 A: I think there's a misunderstanding here: there is one method for building a model in which choice breaks, and the point is that to get a model in which choice fails and some large cardinal axiom $(*)$ holds, we start with a model in which $\kappa$ has $(*)$, and then cause a failure of AC sufficiently far above $\kappa$ that $\kappa$ still satisfies $(*)$ in the resulting model.
In this example, if there is an elementary embedding $j$ of $L(V_{\lambda+1})$ into itself with critical point below $\lambda$, then $j$ is also an elementary embedding of $L(W_{\lambda+1})$ into itself with critical point below $\lambda$ as long as $W$ is any forcing extension of $V$ such that $W_{\lambda+1}=V_{\lambda+1}$. So if we start with a $V\models I_0$, and add a failure of choice by taking a symmetric submodel of an extension of $V$ by a forcing which is sufficiently closed (so doesn't alter $V_{\lambda+1}$), the resulting model will still satisfy $I_0$.

EDITED FOR CLARITY: Note that all we're using is that the $I_0$ axiom depends only on an initial segment of the universe; so breaking choice above that segment won't affect things. This isn't entirely obvious, since unlike e.g. inaccessibility, the $I_0$ axiom seems to refer to a proper-class sized object - namely, $L(V_{\lambda+1})$ and the embedding $j$. However, the statement "$x\in L(y)$" is absolute, and so things are no more complicated (from a killing-choice-while-preserving-the-axiom point of view) than the case of $I_1$, which is explicitly about the set $V_\lambda$. 
In principle, we could imagine variations on the $I_0$ axiom of the following form: "There is an elementary embedding of $M(V_{\lambda+1})$ into itself with critical point below $\lambda$," where "$M(-)$" is shorthand for "the class of $x$ such that $\varphi(x, -)$" for some $\varphi$. So long as $M(-)$ is always guaranteed to be an inner model, this could be interesting, and if (the formula $\varphi$ associated to) $M$ were sufficiently non-absolute, then there wouldn't be an obvious way to kill choice while preserving "$I_0(M)$". However, I'm unaware of anything interesting along these lines.
