Suppose $M$ is a model of $\sf ZF$ that is externally bijective to an element $k \in M$. Obviously if $j$ denotes such an external bijection, then it cannot be used in Separation and Replacement within $M$, because the range of $j$ from $\mathcal P^M(k)$ would be a subset of $k$ that is bijective to $\mathcal P^M(k)$ by $j^{-1}$, and using Separation one can easily recover the diagonal which would be an element of $M$, and thus $M$ would no longer be bijective to $k$.

Would it be safe to use $j$ in stratified instances of Separation and Replacement within $M$? Where "stratified" is defined after Quine with the addition that $j(x)$ and $x$ receive the same type during stratification.

The main context is whether the stratification criterion can provide immunity from paradoxes when internalizing external functions inside models of $\sf ZF$. If that holds, then it may constitute a powerful tool, since we may use it in internalizing automorphisms, embeddings, etc..

Suppose $M$ is a model of $\sf ZF+\neg AC$ that is externally bijective to an element $k \in M$. Obviously if $j$ denotes such an external bijection, then it cannot be used in Separation and Replacement within $M$, because the range of $j$ from $\mathcal P^M(k)$ would be a subset of $k$ that is bijective to $\mathcal P^M(k)$ by $j^{-1}$, and using Separation one can easily recover the diagonal which would be an element of $M$, and thus $M$ would no longer be bijective to $k$.

Would it be safe to use $j$ in stratified instances of Separation and Replacement within $M$? Where "stratified" is defined after Quine with the addition that $j(x)$ and $x$ receive the same type during stratification.

The main context is whether the stratification criterion can provide immunity from paradoxes when internalizing external functions inside some models of $\sf ZF$. If that holds, then it may constitute a powerful tool, since we may use it in internalizing automorphisms, embeddings, etc..