A couple of months ago, Agda (you play Agda without installing it at the Agdapad) obtained universes up to $\mathcal{U}_{\omega\cdot2}$, whereas before we just had $\mathcal{U}_\omega$. So yes, iterating this beyond $\omega$ is definitely possible, and in some circumstances also useful. (Why stop at $\omega\cdot2$? It's the smallest extension such that every type has a type and such that we can quantify over the levels below $\omega$.)

In addition to @RodrigoFreire's nice answer, there is a double negation translation from ZF to IZF, but not from ZFC to IZF. (IZF is basically ZF without LEM. Considering IZF+Choice isn't very useful, as IZF+Choice proves LEM and hence ZFC.) That is, usage of the law of excluded middle can always be mechanically eliminated from any ZF-proof (at the expense of introducing lots of double negations in the formulation of the statement proven). For ZFC this is not the case. In this sense ZF is much closer to being constructive than ZFC.

Welcome to MathOverflow, masala! Yes, we can add various forms of the law of excluded middle to dependent type theory, similar to how we can add the law of excluded middle to intuitionistic logic. A reference includes the introduction of the homotopy type theory book and more specifically Section 3.4.

@JordanMitchellBarrett: But just so you know, the statement that $\textbf{Set}$ is the terminal Grothendieck topos is not some deep insight about the category of sets, because the notion of a Grothendieck topos refers to $\textbf{Set}$. In fact, there is a relativization: For any (elementary) topos $\mathcal{E}$, $\mathcal{E}$ is terminal in the category of "Grothendieck toposes over $\mathcal{E}$" (more formally known as "elementary toposes which are bounded over $\mathcal{E}$).

Simon, very good answer. I'm wondering, do you have an analogue for the end extensions in set theory?

Unfortunately I also don't know a precise reference. The construction has certainly long been known in the topos community; it is an instance of "sheaves with respect to the regular topology". Perhaps this helps in tracking down a reference.

Welcome on MO, Anna! I too like that proof very much. It's the workhorse of my favourite approach to diagram chasing in abelian categories: use the internal language of the resulting sheaf topos. (If desired, the definition of internal language can be unrolled to eliminate all mentions of sheaves and even sets, working just fine in restricted predicative foundations, yielding a convenient interface to this little jewel by George Bergman.

@Franka Thank you for providing motivation! I just added the proof to a paper draft of mine, please have a look at Footnote 9 in Section 2.2 and share any difficulties in following the argument so that I can improve it, for the benefit of all who are interested in this curious injection. :-) Section 2 of this paper aims to give a leisurely introduction to the internal language of the effective topos and is hopefully readable even without extensive knowledge of toposes.

@Franka I meant $\mathbb{R}$, but indeed now that you say it I recall that Andrej proved it for $\mathbb{N}^\mathbb{N}$. Slides illustrating Andrej's proof are here (see slide 24/25). The argument easily adapts to $\mathbb{R}$, this is a fun exercise; if you want me to spell out the details, I'll gladly do so!

This answer is spot on! I'd like to contribute the realizability topos given by infinite-time Turing machines as a further intriguing environment. Any topos has an "internal logic", but the one of this one is particularly challenges many mathematical intuitions shaped by classical logic. In this topos, there is no surjection $\mathbb{N} \to \mathbb{R}$ (as you would expect from CLASS), but there is an injection $\mathbb{R} \to \mathbb{N}$. This observation is due to Andrej Bauer.

@ValeryIsaev: Can you clarify? The condition "$\forall x,y : M. \neg\neg(x = y) \Rightarrow x = y$", interpreted in the internal language, is exactly the condition for the object $M$ to be separated with respect to the $\neg\neg$-topology.

@Andrej: It is consistent with ZF that the zero module is the only injective module. Hence in some sense there can be no constructive examples. (However, if you believe in the existence of enough injective modules in the metatheory, then sheaf toposes over locales will also contain enough injective modules, see Theorem 3.8 of this note.) All the definitions of injective modules which I know are constructively equivalent. However, it might be possible to ponder a "dynamical variant". Daniel Wessel is the person to ask!