Thanks. I edited to fix.

Thanks! Do you know if this has been observed before in the literature? It seemed like something that would have been noticed before, so I was expecting to find it in one of the standard computability textbooks but could not see it.

This is the same point as Zhen Lin, but just to emphasis it, this is not in any way problematic and it is very misleading to say simplicial sets is "contradictory up to homotopy" because the subobject classifier for the 1-topos has very little to do with the subobject classifier of the $\infty$-topos. When we're working with a model category, I would refer to the latter as "homotopy subobject classifier," but I'm not sure how standard that is. Simplicial sets is boolean as an $\infty$-topos, so the homotopy subobject classifier is 2, which is not connected.

I assume you're thinking of classical logic? In intuitionistic logic there are some conservativity results in this area.

@Jem I guess it's not really spelt out in that paper (IIRC Håkon has explained it better other places but I don't know a reference offhand). $V$ really is a retract of $M$ - its the subtype of "hereditary embeddings" and you can construct the map $M \to V$ by recursively taking the image factorisation. In particular you explicitly have a section of the map $M \to V$ (the inclusion) so there isn't any choice needed to show it is surjective.

@UlrikBuchholtz I thought that at first, but I think that adding enough universes/inaccessibles and propositional resizing messes it up: The only axiom of IZF missing from Power-CZF is full separation. If you have a set X sitting inside an inaccessible set V, then an instance of full separation in V becomes an instance of bounded separation in the next universe level up, say $V'$, and so we get $Y \subseteq X$ with $Y \in V'$. Then in order to get propositional resizing we want P({1}) to be the same in V and V', which combined with function regularity lets us show Y must already belong to V.

I'll think how to phrase it a bit better - I did intend it to mean "for each n, an axiom stating...".

Having said that, you can read off a more explicit description where the 2 steps are combined. In general existential quantifiers will need to be combined with double negation, but $(\exists ! y)\varphi(x, y)$ is equivalent to $\mathsf{IsContr}(\Sigma_{y : V_{\neg\neg}} \varphi(x, y))$ which only uses type constructors preserved by the inclusion from sheaves to the original universe.

This is using the HIT cumulative hierarchy for the interpretation - the Aczel hierarchy is just being used to show that the HIT cumulative hierarchy exists. Also, the idea is to do a 2-step construction where the model of $\mathbf{ZF}$ is constructed in the internal logic of the reflective subuniverse, which satisfies LEM, so it's enough I think to interpret $\mathbf{ZF}$ given LEM and the HIT cumulative hierarchy, which is in the HoTT book.

The proof I had in mind works, although it requires a HIT that is technically just outside the ones that I listed as "standard". It's a little long, so I'll edit it into the answer.