The Mostowski Collapse Lemma states that for all sets $S$ and extensional, well-founded relations $R$ on $S$, there exists a transitive set $T$ such that $(S, R)$ and $(T, \in_T)$ are isomorphic. It is often used, for instance, to collapse a well-founded model of ZFC to an isomorphic transitive model.
In fact, we can slightly strengthen the lemma to say that for all sets $S$ and well-founded relations $R$, there is a (necessarily unique) function $f$ with domain $S$ such that for all $s \in S$, $f(s) = \{f(r) \mid r R s\}$. Call this the "general collapse lemma", and call $f$ the collapsing function for $(S, R)$. It's straightforward to see using $\in$-induction that if $R$ is extensive, then $f$ is injective; thus, $f : S \to f(S)$ is an isomorphism from $(S, R)$ to $(T, \in_T)$, and the Mostoswki Collapse Lemma holds.
The usual proof of the general collapse lemma is a straightforward application of well-founded recursion. Well-founded recursion is in turn proved using the axioms of full separation and replacement. Unfortunately, CZF does not have full separation, only $\Delta_0$ separation.
Can the general collapse lemma be proved in CZF? Can the Mostoswki Collapse Lemma be proved in CZF?
Note that the general collapse lemma is equivalent to full well-founded induction, while the Mostoswki Collapse Lemma is equivalent to full well-founded induction for extensional relations. Thus, we could also ask whether CZF proves well-founded induction, and whether CZF proves well-founded induction for extensional relations.
Edit: if we add the existence of $W$-types, then this follows. More precisely, we need the following axiom: for all families of sets $\{B_a\}_{a \in A}$, there is a smallest set $W_{a \in A} B_a$ such that for all $a \in A$, for all $f : B_a \to W_{a \in A} B_a$, $(a, f) \in W_{a \in A} B_a$.
We can define a relation $\prec = \{(f(b), (a, f)) \mid a \in A, f : B_a \to W_{a \in A} B_a, b \in B_a\}$. It’s straightforward to see that $\prec$ is well-founded. Less trivially, we can use $\in$-induction to prove all instances of well-founded induction for $\prec$. The trick here is that $\prec$ is a sub-relation of the transitive closure of $\in$ - this follows from the precise definitions of functions and ordered pairs in CZF.
Now consider some $C$ and well-found $\prec$ on $C$. Then define $B_c = \{x \in C \mid x \prec c\}$. Then we have the obvious function $f : C \to W_{c \in C} B_c$, given using $\Delta_0$ well-founded recursion by $f(c) = (c, f|_{B_c})$. Now $f$ is injective, and for all $x, y \in C$, we have $x \prec y$ if and only if $f(x) \prec f(y)$. Thus, we can prove full well-founded induction for $(C, \prec)$.
Unfortunately, I’m fairly sure CZF doesn’t prove the existence of $W$-types.