The well-known reflection principle for classical Zermelo–Fraenkel states:

For any formula $\varphi(x_1,\ldots,x_n)$ of the language of ZFC with free variables $x_1,\ldots,x_n$, ZFC proves $$ \forall M_0. \exists M \supseteq M_0. \forall x_1,\ldots,x_n \in M. (\varphi(x_1,\ldots,x_n) \Leftrightarrow \varphi^M(x_1,\ldots,x_n)), $$ where $\varphi^M$ is the $M$-relativization of $\varphi$.

Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.

Surely this has been studied before, but I wasn't able to track down a reference.

Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.

The well-known reflection principle for classical Zermelo–Fraenkel states:

For any formula $\varphi(x_1,\ldots,x_n)$ of the language of ZFC with free variables $x_1,\ldots,x_n$, ZFC proves $$ \forall M_0. \exists M \supseteq M_0. \forall x_1,\ldots,x_n \in M. (\varphi(x_1,\ldots,x_n) \Leftrightarrow \varphi^M(x_1,\ldots,x_n)), $$ where $\varphi^M$ is the $M$-relativization of $\varphi$.

Question. Does the analogous theorem hold with ZFC replaced by IZF, intuitionistic Zermelo–Fraenkel? All proofs of the reflection principle for ZFC that I know of don't obviously carry over to IZF, firstly because of the failure of Scott's trick and secondly because we cannot, unlike in classical texts, assume without loss of generality that formulas don't contain universal quantifiers.

Surely this has been studied before, but I wasn't able to track down a reference.

Motivation. With such a reflection principle in place, we could mimic the definition of ZFC/S, a conservative extension of ZFC useful for category theory, to create IZF/S. The reflection principle is what powers the automatic transfer from a given theorem formulated, for instance, for all small groups, to one formulated for all groups, and this leap shouldn't require non-intuitionistic techniques.