A common schema in intuitionistic, constructive set theories is that of $\it{\Delta_0}$ separation:
$$ \forall x\exists y\forall z(z\in y\leftrightarrow z\in x\wedge\phi(x, z))\text{ provided $\phi$ is a $\Delta_0$ formula} $$
So chosen as $\Delta_0$ sets are clearly predicatively defined, and full separation is known to be implied by $\mathsf{LEM}$, suggesting a non-intuitionistic nature to it. However Aczel provides a type-theoretic justification for a different separation principle, $\textit{small separation}$:
$$ \forall x\exists y\forall z(z\in y\leftrightarrow\exists w(w\in x\wedge\phi(x, w)\wedge w = z)) $$
with no restrictions on $\phi$. The latter is equivalent to the former without restriction on $\phi$ if $\phi$ is (internally) extensional in $w$ (that is, it is provable $w = z\rightarrow \phi(x, w)\leftrightarrow\phi(x, z)$), and specifically all $\Delta_0$ formulae are extensional by a routine induction on syntax. Thus, small separation implies all instances of $\Delta_0$ separation.
Does the converse hold, and if not, how might $\Delta_0$ separation be characterized non-syntactically, or the relative strengths of these axioms be compared?
It is known in classical $\mathsf{KP}$ that $\Delta_0$ separation implies stronger separation, in fact every instance of absolute separation, separation for absolute formulas. This is not known to be true of intuitionistic $\mathsf{KP}$, however it is known that $\mathsf{KP}$ and $\mathsf{CZF}$ are interpretable in each other, suggesting that at least relative to $\mathsf{CZF}$, absolute separation should hold. It's not then clear to me if and how absoluteness would apply to proving all instances of small separation.
Intuitively, to use small separation to show an element is in $y$, one would have to produce a witness for $w$. This should effectively bound all quantifiers in $\phi$ by the set of all "presently constructible" sets, restoring predicativity and suggesting that every application of small separation begets an equivalent application of $\Delta_0$ separation, but I'm suspicious that impredicativity has snuck in here and that a metatheoretic proof cannot be extracted from this argument.
$\Delta_0$-separation admits a rather elegant semantic interpretation. We consider a first-order theory of categories with terminal elements. The sole predicate is equality on morphisms. A $\Delta_0$ formula in this theory is one in which for every quantifier there is an object $X$ for which the variable ranges over the morphisms $1\rightarrow X$.
Structural $\Delta_0$-separation
For every $\Delta_0$ formula $\phi$, there exists a mono $s : S\rightarrowtail X$ such that $x : 1\rightarrow X$ factors through $s$ if and only if $\phi(x)$
This can be expanded in the obvious way to full structural separation, with most of the sequel extending in the expected way to the usual consequences of inviting full separation into your set theory.
Structural $\Delta_0$ separation is a nice categorical property, as the following shows
Theorem [Shulman]
A finitely complete category is Heyting and constructively well-pointed (that is, its initial object is a separator, projective, indecomposable, and admits no morphisms to the terminal object) if and only if it satisfies structural $\Delta_0$-separation.
If objects interpret sets and their elements are identified with global elements, then this is a reasonable interpretation of material $\Delta_0$-separation in the sense that $S$ interprets $\{x\ |\ \phi(x)\}$ up to isomorphism. This can be made precise in the following sense:
Theorem [Shulman]
A $\Pi$-pretopos* with an natural numbers object** satisfying $\Delta_0$-separation interprets a material set theory satisfying material $\Delta_0$-separation
*I have intentionally copied this condition verbatim; my grasp on category theory is weak but I believe this is unnecessarily strong and a constructively well-pointed Heyting category would suffice
**Similar note. The finitist could probably do with only induction in the metatheory
This is not immediate, as our theory of categories only identifies sets up to isomorphism (even in $\mathbf{Set}$: this is a trivial consequence of having no predicate on objects). Instead the interpretation works by essentially abusing the natural numbers object to create a local W-type to interpret sets a la Aczel. Hamfisted, but effective.
Our first theorem gives assurance that $\Delta_0$ separation is the "right" notion of separation in predicative minimalism, as a constructively well-pointed Heyting category is an arguable semantic lower bound for set theories we might be interested in.
This is all good, but it doesn't really answer the question: I've only kicked the can down the road into a theory of categories. And to an extent, that's where it'll have to stay. the categorical perspective at least makes intuitively precise what the strength of $\Delta_0$-separation is: it is separation quantified over objects of the category, at least so far as there is enough internal structure to prove factorization. We have very few canonical choices left to extend the structure. We could add local cartesian closure, which would only be of interest in particularly weak theories, or we could add power objects/subobject classifiers, which bring us Boolean-ness away from $\mathbf{Set}$.
Besides this observation, being the strict lower bound specified by the constructively well-pointed Heyting category is in and of itself the best characterization of $\Delta_0$ formulae.
So what of small separation? How does it compare? Small separation doesn't admit a clear candidate for a structural analog, as objects cannot be identified beyond isomorphism, so separation holding up to isomorphism implies (at least up to laundering through the constructions of Shulman) that separation holds, which is demonstrably unconservative, both as it's known that full separation interprets second-order arithmetic, and that there are models of $\mathsf{CZF}$ refuting full separation (although, interestingly, not to my knowledge also refuting $\mathsf{REA}$, though they should exist as $\mathsf{CZF + REA}$ is interpretable in $\mathsf{KPi}$ which is weaker than second-order arithmetic).
This leaves us with the elephant in the room: if by every inspection small separation is separation, then I must be mistaken; what is actually justified by Aczel's interpretation?
The missing piece is that in Aczel's justification, the type interpreting $\phi$ must be small. As the type of sets is not small, unbounded quantification is interpreted by large $\Sigma$ types, whereas bounded quantifiers are small. Ergo, the justified separation formulas are precisely those with $\Delta_0$ $\phi$. A subtle point, but critical. This remains true even if full W-types are added to the type theory: semantically, this upgrades the model category to a $\Pi W$-pretopos, but still only justifying $\Delta_0$-separation (now stronger thanks to the additional objects). This explains semantically why $\mathsf{CZF + REA}$ for example does not explode in proof-theoretic strength.