Grothendieck topoi as a constructive property

Question

This question is inspired by Homotopy type theory, but I believe it can be thought about also in other constructive foundations.

In HoTT the question could be stated as follows:
Given a definition of Grothendieck topos $C$ as a geometric embedding into presheaves on some category $site$, call it $S : Category \rightarrow Type$. This is obviously a structure, rather than property. Is there a property $P : Category \rightarrow Type$ such that $P$ is a homotopy proposition with $P(C)$ and $S(C)$ implying each other?

In general here is an idea working in usual (set-based) CLASSICAL category theory, to obtain similar behavior;
Using well-ordering of cardinals and Giraud's theorem, the structural bit of Giraud's theorem is the accessiblity part of local presentability. To obtain something property-like with choice, one could pick the least $\kappa$, for which $C$ is $\kappa$-accessible. This should possibly work in impredicative HoTT with choice, but I havent checked whether the truncated choice in HoTT is actually enough.

Are there other classically equivalent characterizations of Grothendieck topoi that could be made reasonably property-like and potentially constructive?
One definition I wonder about in particular is the definition as a Set-bounded topos as this definition relativizes. Here the usual definitions involve picking a bound or picking a fibered generating family, which there could be many. All the equivalent characterizations I am aware of, of bounded geometric morphisms are structure-like.

Here are options I wondered about that I failed to determine truth of:

1. Is there always a unique standard site? I dont think so but I am not aware of a counterexample.
2. Does the full subcategory of category of (standard?) sites, on sites which result in the same Grothendieck topos $T$, have initial or terminal objects?

I doubt this is possible and an attempt to make it precise metatheoretically for HoTT + any consistent rules that would have normalization, would be the following conjecture: There can be no type family $GrothProp : Category \rightarrow Type$ in any constructive strongly normalizing extension of HoTT; such that $(\forall C. isHProp(GrothProp(C))) \times (\forall C. GrothProp(C) \rightarrow Groth(C)) \times (\forall C. Groth(C) \rightarrow GrothProp(C))$,

where $Groth$ is the definition in terms of site + geometric embedding. In other words a very nice propositional definition of Grothendieck topoi would be a strong sort of constructive taboo in HoTT.

Answer 1

One possible answer is that in his 1981 paper "Notions of topos", Ross Street proved that with a fixed universe to define "small" and "large", if $C$ is a locally small and "moderate" category, the latter meaning that its set of objects is large but no larger than the size of the universe itself, then it is a Grothendieck topos if and only if its Yoneda embedding $C \to [C^{\rm op}, \rm Set]$ (which exists because $C$ is locally small, although $[C^{\rm op}, \rm Set]$ is not locally small) has a left exact left adjoint. In Street's words, "the only canonical choice of site is the topos itself."

If memory serves, Street's proof is not very constructive, involving a transfinite induction over all small ordinals, perhaps even well-ordering the objects of the category. But perhaps there is some constructive analogue; I haven't thought about it.