@Z.M I think you are right; however, I still wanted to find internal characterization of dimension, in order to be able to carry out as much work as possible internally to the (little or big) Zariski topos.

To tackle concerns of impredicativity, instead of the locale of real numbers, which is the classifying locale of the theory of Dedekind cuts, we can also consider the classifying topos of this theory. Like all classifying toposes, this is a category of sheaves over the base, and is impredicative only insofar the base is. In predicative mathematics, where the category of Sets is not an elementary topos, this category of sheaves will also no longer be an elementary topos, but still be an arithmetical universe. Simon's second construction applies also for classifying arithmetic universes.

@aws Just to confirm, yes, Andrej's paper shows that the realizability topos built using ITTMs has an injection $\mathbb{N}^\mathbb{N}\hookrightarrow\mathbb{N}$, but his argument is easily adapted to $\mathbb{R}\hookrightarrow\mathbb{N}$. (See Footnote 10 of this survey of mine for a somewhat self-contained argument.) — Only in the trivial topos there can be a bijection $\mathbb{N}\cong[0,1]$. A topos containing a surjection $\mathbb{N}\to\mathbb{R}$ has recently been found by Andrej and James Henson.

Very nice! Your proof is similar to this proof (Theorem 4.25) of Benno van den Berg and Jaap van Oosten's result that in the effective topos, Heyting arithmetic is categorical in the sense of admitting (up to isomorphism) exactly one model.

I wrote up a site-independent characterization, along with a commentary of several inequivalent options, here. I believe it could be relevant to you, because avoiding Zorn was one of the major motivations for this text. However, let me also clearly state that I failed to constructivize the result you mention, and that the text is in the middle of a substantial revision. The new version will prove, constructively, that every sheaf of modules embeds into a flabby sheaf of modules.

@ZhenLin You are right; nowadays we do have a syntactic description of the fppf topos (Section 21.2 of these notes of mine, but Wraith's conjecture, which would yield a much nicer description, is still open.

Good point, @LeoAlonso! What about the naive definition? After all, there is a good notion of point of a Grothendieck topos, and any geometric morphism induces a map between the points.

In case you are thinking of flabby resolutions as a substitute for injective ones: I'm in the middle of a revision of this paper on injective and flabby objects in toposes. The main new result will be that there are enough flabby modules in any elementary topos with an NNO. However, in the absence of Zorn's Lemma, these (still) fail to have the exactness properties which sheaf cohomology requires. A better variant of the notion of flabby objects will be subject to a forthcoming paper.