It's not enough to have dependent choice. DC holds in the effective topos, but the Fan theorem does not, but the "Kleene tree" argument.

Yes. To connect this with formal topology, every formal topology is in particular a site (a site where the underlying small category is a poset), and I would guess that sheaves on that site gives an explicit description of the classifying topos.

But actually I think it should be an injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$ - I'm not sure if it extends to the real numbers.

Sorry, I meant $[0,1] \to \mathbb{N}$ for the injection.

Cantor's argument shows that if $[0,1]$ has decidable equality there is no surjection $\mathbb{N} \to [0,1]$ but there can still be an injection. The main topos theory example is realizability on infinite time Turing machines.

In the paper at doi.org/10.1016/0168-0072(94)00030-7 Palmgren put some syntactic restrictions on what formulas you can transfer. I think it has to prevent this kind of argument, since otherwise it would work fine in $\mathbf{HA}_\omega$and he claimed the theory there is conservative over $\mathbf{HA}_\omega$.

In the reference I mentioned they work with power set, but the same argument should work in general, just giving a class sized complete Heyting algebra. You can then talk abut the collection of all complete Heyting algebras that arise from small lattices in this way. This would not give you every complete Heyting algebra, necessarily, but it would be a large enough collection of them to have a completeness theorem.

Sorry, I confused Dedekind MacNeille completion with a similar construction that preserves any joins already existing in the poset (Theorem 6.13 in Chapter 13 of Troelstra and Van Dalen, Constructivism in mathematics, vol 2). For that one you get a complete Heyting algebra out given a Heyting algebra to start with, but maybe not for Dedekind-MacNeille.

There are a few references comparing the consistency strength of variations of CZF with classical theories, but I think Rathjen, Griffor, Palmgren, Inaccessibility in constructive set theory and type theory is probably the most standard one regarding CZF inaccessible sets.

I guess actually the most relevant approach would depend on why you are interested in complete Heyting algebras and what you want to do with them. As an example, you can use complete Heyting algebras to build models of theories in intuitionistic logic, so you can prove, for example, the soundness theorem for intuitionistic logic for all (class sized) complete Heyting algebras specified as the Dedekind MacNeille completion of a poset, which would also have a completeness theorem.