Good question, especially because verifications like these are sometimes swept under the rug. But $g$ being given in a somewhat canonical fashion does not guarantee that actually $g = RF(f)$; in particular, this might hold only up to sign. In computer science, there is something called "theorems for free" which is probably relevant to this question.

Phrasing @David's comment as a fuzzy slogan: In a category, not every triangle commutes, but every tetrahedron (or higher structure) of morphisms made from commutative triangles commutes.

(continued) If we define the spectrum in a more sensible manner, for instance as a locale, then being an epimorphism will imply but won't be equivalent to being surjective on all stalks. (A sufficient condition ensuring equivalence is that the Boolean Prime Ideal Theorem holds. This is slightly weaker than the full axiom of choice.)

@FrançoisG.Dorais: Even constructively, in the absence of both choice and the law of excluded middle, a morphism is an epimorphism in $\mathrm{Sh}(X)$ (in the categorical sense) if and only if it is surjective on all stalks. This remark is for topological spaces $X$. The situation is different (even classically) for locales instead of topological spaces. Your comment is therefore quite relevant, because while it's possible to define, in a context without choice, the spectrum of a ring as a topological space, the resulting space won't have the expected universal property. (continuing)

I believe that "Noetherian" can be weakened to "quasicompact".

That's very clear. Thank you for taking the time for spelling out the verification!

I was recently shocked to learn that, if Zorn's lemma holds in the metatheory, it also does so internally to any localic topos (not only toposes of sheaves over spaces which are close to being discrete). This is in the Elephant. However, you're right in that the axiom of choice does not descend in this way, and maximal ideals are only really useful in the presence of the law of excluded middle (for instance the proof that maximal ideals are prime requires this). The axiom of choice is equivalent to Zorn's lemma + law of excluded middle.

I don't believe that the definition "$e(p) = \sup\{1 \,|\, p \}$" works, since the MacNeille reals are only conditionally complete (any inhabited subset with an upper bound has a least upper bound). One could fix that by changing the definition to "$e(p) = \sup(\{0\} \cup \{1\,|\,p\})$". In any case, @Sridhar: One can prove without any form of choice that for any map from the naturals to the MacNeille reals, there is a MacNeille real which is not in the image of that map. That is to say, the MacNeille reals are constructively uncountable in a strong sense.

(continued) For this, let $M$ be the machine which searches all $T$-proofs for a proof of "$M$ halts" or "$M$ doesn't halt" and, upon finding such a proof, performs the opposite of what the proof is claiming. Assume that $T$ proves that $M$ halts or that $T$ proves that $M$ doesn't halt. Looking at the first-found proof of either statement, we can then deduce with some work that $T$ is inconsistent.

Andreas Kaseorg taught me today how to remove the soundness hypothesis. Let $M$ be the machine which looks at all $T$-proofs and stops as soon as a proof of "$M$ doesn't halt" has been found. If $T$ shows that $M$ doesn't halt, then $M$ actually halts, then $T$ can prove this fact, and hence $T$ is inconsistent. Hence "$M$ doesn't halt" is a true but unprovable statement. We can further incorporate a version of Rosser's trick to show Gödel's incompletenesstheorem in full generality. (continuing)

@Mario: Yes, a few beginnings are described on pages 11ff. of these notes of mine. However, it wasn't developed with HoTT in mind, that is, it's strictly one-categorical and no higher homotopies are in sight.