@Zhen Lin: Just that no confusion arises, you refer to Hakim's construction of an internal spectrum. The relative spectrum commonly used in algebraic geometry is related to Hakim's, but different in general. (The most glaring difference is the following: Let $(X,\mathcal{O}_X)$ be a locally ringed topos. Let $\mathcal{A}$ be an $\mathcal{O}_X$-algebra. Then $(X,\mathcal{A})$ is a ringed topos. The morphism $\mathrm{HakimSpec}(X,\mathcal{A})\to(X,\mathcal{O}_X)$ is not a morphism of locally ringed toposes. In contrast, the morphism $\mathrm{RelSpec}(X,\mathcal{A})\to(X,\mathcal{O}_X)$ is.)

Regarding the question in your last paragraph: No, taking the "SPEC" of the ringed-space product doesn't yield the correct product in the category of locally ringed spaces (or schemes, those are the same). You have to use a refined construction which takes the structure sheaves of the factors into account; else the "projection morphisms" $X \times Y \to X$ and $X \times Y \to Y$ won't be morphisms of locally ringed spaces (even though source and target are locally ringed).

Apparently, there is some confusion as to what the right meaning of "pullback (in an appropriate topos sense)" is.

@ChristopherTownsend, that claim of Peter is discussed on the nForum, with no clear consensus. One thing to note is that the "pullback square" in question only commutes up to a non-invertible natural transformation.

... then you can constructively only justify $\neg\neg \exists x (\text{the key is at position x})$. (This real-world example doesn't fully work out since it confuses absolute mathematical truth with personal knowledge.)

For a general statement $\varphi$, not of the special form required by Friedman's trick, the story goes as follows. Believing that $\varphi$ doesn't fail to hold -- i.e. believing $\neg\neg\varphi$ -- is constructively weaker than believing that $\varphi$ holds. For instance, a proof of $\exists x(\ldots)$ requires an explicit witness of $x$, while a proof of $\neg\neg\exists x(\ldots)$ doesn't. A real-world example is the following: If in the morning you can't find the keys to your apartment, but you do know that they must be somewhere (as you used them to unlock the door last night), ...

The question is subtle for the following reason: Peano arithmetic is conservative over Heyting arithmetic (i.e. intuitionistic Peano arithmetic) with respect to statements of the form "$\forall \exists (\ldots)$" (where no quantifiers may occur in the bracketed subexpression). This result goes by the name Friedman's trick or Friedman translation. The statement that a particular Turing machine halts on every input is of such a form. Therefore any classical termination proof gives rise to a constructive termination proof.

On page 9 of Bhargav Bhatt's lovely notes on the étale topology there is the following statement: "For an analytic space $X$, the étale topos $Et(X)$ is equivalent, as a category, to the standard topological topos $Top(X)$ whose cohomology is, by definition, singular cohomology." The étale site of an analytic space $X$ is defined just like in the algebraic case, only "with (analytic) local isomorphisms replacing the étale morphisms".

For the benefit of other constructively minded readers, here is an intuitionistic proof that $q$ is surjective on objects. Consider the category $\mathcal{D}$ with objects the subsets of $\{\heartsuit\}$ and with exactly one morphism between each pair of objects. Consider the functor $G : \mathcal{C}[W^{-1}] \to \mathcal{D},\,Y \mapsto \{ \heartsuit\,|\, Y \in \mathrm{im}(q) \}$. Also consider the functor $H : \mathcal{C}[W^{-1}] \to \mathcal{D},\,Y \mapsto \{ \heartsuit \}$. Then $G \circ q = H \circ q$, so $G = H$. Thus $Y \in \mathrm{im}(q)$ for any $Y \in \mathcal{C}[W^{-1}]$.

In this picture, representable functors generalize free modules. Recall that $R^n \otimes_R M \cong M^n$ for ordinary modules $M$. Similarly, we have $\mathrm{Hom}(\cdot, n) \otimes G \cong G(n)$ for functors $G : \mathcal{C} \to \mathrm{Set}$ and objects $n \in \mathcal{C}$. Incidentally, looking at the coend formula, we see that $\mathrm{Hom}(\cdot, n)$ can be interpreted as a "delta distribution" concentrated at $n$.

This does not answer your question in any way. Just want to direct interested readers to the note Sheaves and Homotopy Theory by Daniel Dugger, where the cocompletion business is explained in very accessible terms with lots of intuition. Specifically, $F$ and its right adjoint, the forgetful functor from cocomplete categories to arbitrary categories, are discussed. The size issues which Qiaochu refers to are ignored though.

Regarding John's comment, the beautiful notes of Emily Riehl have moved here.

@user4676: It is true that the category of semisimplicial sets has all limits and all colimits. However, these do not behave as one would geometrically expect. This can already be seen with empty limits: The terminal object is not the one-point space, but an infinite-dimensional sphere. The deeper reason for this bad behaviour is the paucity of morphisms in the category of semisimplicial sets. Also note that the geometric realization functor from semisimplicial sets to topological spaces does not preserve (co-)limits.