@HeinrichD: I loved this thread as well and am really grateful for you posting that question. I'd like to acknowledge you in my PhD thesis, since this thread inspired a small but cute part of it. Please contact me by mail at [email protected] to let me know your surname (unless you want to stay pseudonymously, of course).

Exactly. Yes, it is a scheme since $f$ is a local homeomorphism: For any point of $\mathrm{Ét}(\mathcal{E})$ there is an open neighbourhood $U$ which is homeomorphic to some open subset $V$ of $X$, and $(f^{-1} \mathcal{O}_X)|_U$ corresponds to $(\mathcal{O}_X)|_V$ under this homeomorphism.

Yes, and afterwards we can equip $f_! f^{-1} \mathcal{O}_X$ with the structure of an $\mathcal{O}_X$-module. But we also directly use the versions of these functors for modules instead of abelian groups.

@Harry: The algebraically defined sheaf of modules of Kaehler differentials does (of the sheaf of smooth functions over the sheaf of locally constant functions) does not coincide with the usual sheaf of differential forms as considered in differential geometry. Only its double dual does. (Unraveling the definitions, this is mostly a triviality.)

Very nice answer. Just a remark to the second-to-last paragraph: The category of affine $S$-schemes which are locally of finite type over $S$ is essentially small. This is good to know, since by Grothendieck's comparison lemma the category of Zariski sheaves over $\mathrm{Sch}/S$ is equivalent to the category of Zariski sheaves over $\mathrm{Aff}/S$ (both with the same finiteness condition). The latter is a honest category in that -- since $\mathrm{Aff}/S$ (with the finiteness condition) is essentially small -- you don't have any set-theoretical issues with constructing it.

@Harry: You can also construct the structure sheaf of $\operatorname{Spec} A$ by localizing the constant sheaf $\underline{A}$ at the universal filter (the subsheaf given by $U \mapsto \{ f \in \underline{A}(U) \,|\, \text{$f(\mathfrak{p}) \not\in \mathfrak{p}$ for all $\mathfrak{p} \in U$} \}$). I would argue that this is an even better way of constructing the structure sheaf than your B-sheaf proposal, for instance because it makes it easy to verify the universal property of $\operatorname{Spec} A$ and because it's very natural from the point of view of the internal language.

The term "constructive mathematics" is used with related but subtly different meanings. The lingua franca of the mathematical multiverse is "intuitionistic logic" (classical logic is intuitionistic logic plus the axiom of excluded middle). Sometimes "constructive mathematics" refers to doing mathematics using only intuitionistic logic. But sometimes "constructive mathematics" refers to one of several specific schools, where some further axioms are used (for instance Markov's principle or the anti-classical axiom that any function $\mathbb{R}\to\mathbb{R}$ is continuous).

Do you mean by "distinct" "not equal" or "apart"? Also, what is your definition of "eigenvalue"? A real number $\lambda$ such that there exists a vector $v$ with at least one component apart from zero such that $Av = \lambda v$? In this case, if you assume your $n$ eigenvalues to be apart, you at least obtain a linearly independent family of eigenvectors. (Unfortunately, I don't see how these are a generating family.)

I'm too not very familiar with formal topology. Is the pointless locale of surjections $\mathbb{N} \to \mathbb{R}$ an example of the kind you are looking for? It is freely generated by opens $U_{n,x}$ for $n \in \mathbb{N}$ and $x \in \mathbb{R}$ (intended reading: open subset of those surjections $f$ with $f(n) = x$) modulo three sets of relations: $\top = \bigvee_x U_{n,x}$ for all $n$ (read as: "$f(n)$ is defined"); $U_{n,x} \wedge U_{n,y} \leq \sup\{\top\,|\,x=y\}$ for all $n$, $x$, $y$ ("$f(n)$ has only a single value"); and $\top = \bigvee_n U_{n,x}$ for all $x$ ("$f$ is surjective").

As Robert said, the implication $(\neg\neg A \Rightarrow A) \Longrightarrow (A \vee \neg A)$ is not provable in intuitionistic logic. However the related formula $(\forall A{:}\,(\neg\neg A \Rightarrow A)) \Longrightarrow (\forall A{:}\,(A \vee \neg A))$ is. This is because we have $\neg\neg(A \vee \neg A)$.

In the five years since stating the question: Did you settle on a name? Which functor $F$ did you have in mind? Are there some notes where I can read up on your observations?