A Grothendieck topos $\mathcal{E}$ is equivalent to the category of sheaves on some site $Q$. We say a sheaf $X\colon Q^{\text{op}}\to\mathsf{Set}$ is *constant* if it is the sheafification of a constant presheaf, i.e. one that factors through the terminal map $Q^{\text{op}}\to \{\*\}$.


But what if we forget the site $Q$ and consider $X$ as an object in the topos? Can we characterize the property of $X\in\mathcal{E}$ being constant? More specifically, two questions: 


1. Is the property of $X$ being constant dependent on the choice of site $Q$?
2. Is there a way to characterize constant objects in the internal
language of $\mathcal{E}$?



Characterize constant objects in the internal language of a topos?
For the first question: no, the notion of "constant object" doesn't depend on the site. The reason is in Anton's comment: every Grothendieck topos comes with a unique geometric morphism $p : \mathcal{E} \leftrightarrows \mathrm{Set}$, and the constant objects are those in the essential image of $p^\* : \mathrm{Set} \to \mathcal{E}$. In fact, since every object of $\mathrm{Set}$ is not just a colimit but a *coproduct* of copies of $1$, the constant objects are even just those that are coproducts in $\mathcal{E}$ of copies of $1$.


However, I don't think there is any way to characterize constant objects purely using the internal language of $\mathcal{E}$. One reason for this is because the notion of constant object *does* depend on the geometric morphism $p : \mathcal{E} \leftrightarrows \mathrm{Set}$. "Huh?", you say, "didn't you just say that geometric morphism was unique?" Well, yes, so it is... but only once the topos $\mathrm{Set}$ has been fixed! *Any* bounded geometric morphism $q : \mathcal{E} \leftrightarrows \mathcal{S}$ (even between *elementary* topoi) allows us to think of $\mathcal{E}$ as a "Grothendieck topos in the world of $\mathcal{S}$", in which case the "constant objects of $\mathcal{E}$ considered in the world of $\mathcal{S}$" are those in the essential image of $q^\*$. Clearly different choices of $q$ will give different notions of "constant object". But the (finitary) internal language of $\mathcal{E}$ involves only finitary constructions using the elementary structure of the category $\mathcal{E}$, so it is invariant with respect to a "choice of base $\mathcal{S}$"; thus it can't possibly characterize the constant objects.


Infinitary internal languages, by contrast, do depend on the base topos $\mathcal{S}$ to provide a meaning of "infinitary". There are various choices that one might make regarding what to mean by an "infinitary internal language". The "geometric logic" used to describe classifying toposes is infinitary only in allowing infinite disjunctions, but one might also consider infinite conjunctions or infinite strings of quantifiers. If we allow all of these, then here is an infinitary formula that *almost* describes the constant objects:


$$ \bigvee\_{S\in \mathrm{Set}} \exists\_{s\in S}\; x\_s:X. \left(\left(\forall y:X, \bigvee\_{s\in S} y=x\_s\right) \wedge \bigwedge\_{s, t\in S} (x\_s = x\_t \to s=t)\right).$$


This is a *very* infinitary formula: it starts with a disjunction indexed by a proper class! However, Grothendieck toposes are well-powered, so I think one can still make sense of such a formula therein. If you trace through the interpretation of this formula in the natural way, for a fixed set $S$ the infinite quantifier string $\exists\_{s\in S} x\_s:A$ quantifies over the object $X^{\Delta S}$, where $\Delta S$ denotes the constant sheaf at $S$, and the formula inside this quantifier picks out the subobject of $X^{\Delta S}$ consisting of isomorphisms. Thus this formula is asserting "there exists a set $S$ and an isomorphism $\Delta S\cong X$" --- but because the $\exists$ quantifiers are interpreted by images, the truth of this formula internally doesn't imply that $X$ is constant, only that it is *locally* constant (i.e. becomes constant upon pullback to some well-supported object).


This is going to be a problem with any internal logic that's based only on proving propositions. We might hope to get around it by using a full internal "infinitary dependent type theory", and replacing the $\exists$ by a $\Sigma$. I don't know exactly what that means, but even if I did, there would now be a problem with the proper-class disjunction $\bigvee\_{S\in \mathrm{Set}}$ out front, since well-poweredness only allows us to take proper-class-sized unions of subobjects, whereas now we would no longer have subobjects of anything. Perhaps we could mess around with universes. But overall, it seems that the answer is basically "no".


