Just a wild idea: Maybe it'd be worthwhile to formalize synthetic scheme theory as opposed to traditional scheme theory layered upon topology and sheaf theory, similar to how it's worthwhile to formalize synthetic homotopy type theory.

I can confirm your guesses regarding what is classified by the étale topos. A reference in the case of $X = \mathrm{Spec}(R)$ is a very nice paper by Mathieu Anél. What Tim is saying doesn't have an external meaning, since $\mathcal{O}_S$ is not a ring, but a ring object in $\mathrm{Sh}(S)$. However, it has from the internal point of view of $\mathrm{Sh}(S)$; it correctly characterizes the étale topos in the world of toposes over $\mathrm{Sh}(S)$. This doesn't seem to be explicitly written down anywhere. It might be the case that my thesis comes closest.

What is your definition of "rigid tensor category"? For the definition I know, any object is reflexive (that is, the canonical morphism $X \to (X^*)^*$ is an isomorphism).

Martti Karvonen gave a talk on limits in dagger-categories at the PSSL 103. Maybe this is a good starting point?

Excellent question. Tim, in intuitionistic set theory, the correspondence between maps with codomain $Y$ and $Y$-indexed sets still works, so I think your formulation is just fine. I'm wondering: Is even the collection of triples $(X,Y,f)$ where $X$ and $Y$ admit surjections from $\mathbb{N}$ a $\Sigma$-universe, constructively? That seems to be the most basic example classically. But I don't immediately see that it works constructively, because I don't see why fibers should be countable again.

A (as yet unanswered) question of mine is related: mathoverflow.net/questions/263722/…

Very nice! Unlike mine and like Peter's, your proof doesn't require cancellability, so generalizes to modules over rigs. In fact, I believe that your proof can be homotoped to Peter's proof.

To put the claim into the form of a geometric sequent, I was thinking of this: $\langle 1, x \rangle \sim \langle 1, y \rangle \vdash x = y$ (in the context $x,y : X$). With $({\sim})$ I'm referring to the equivalence relation by Mines–Richman–Ruitenberg. If we expand the definition of that relation, we obtain several existential quantifiers (and conjunctions and disjunctions), but no universal quantifiers or implications. Regarding the unnecessarity of baby Barr: Your argument assumes that the topos of sets is Boolean, right? With baby Barr, we can avoid that assumption.

@Peter: I added a few details, and would like to apologize for the messy index-heavy proof. (In German we have a term for this: "Indexschlacht", literally "index battle".) Also thanks for reminding me of the proper notion, I changed "pseudo-ring" to "rig" to not contribute to unnecessary proliferation of terms. Darij: Yes, indeed, thank you; fixed.

I believe that the existence of such a constructive proof [constructively] follows from the existence of the classical proof, since we can apply the baby version of Barr's theorem (the double negation translation followed by Friedman's trick), as the claim can be formulated as a geometric sequent. Do you concur?

@Joel: Regarding your last comment, I don't see how this works. Assuming that T is complete, T shows, for any given Turing machine, that it halts or shows that it doesn't halt. How can you pass from this to a proof in T that there is a halting oracle? I'm confused because T won't prove the reflection principle for T.

@Qiaochu: I believe: Constructively (without any form of choice), the complex numbers built as pairs of Cauchy real numbers are algebraically closed, but the complex numbers built as pairs of Dedekind real numbers might not. (The former embed into the latter.) The algebraic numbers, defined as a subset of either kind of complex numbers, are always algebraically closed. They're also preserved by inverse image under geometric morphisms.

Toby: Couldn't you also add axioms expressing that any object is Kuratowski-finite and discrete? This seems to me to not require an axiom scheme (it does require unbounded quantification).