I’ve put in some of the missing details at internal site.

]]>I understand that the internal language is the general principle here, but I hoped it is not that complicated and lengthy (Elephant book has a relatively long treatment and still most of the details are omitted). Thanks for the second paragraph insight!

]]>I think the definition is a very straightforward (though lengthy) “internalization” of the usual notion of coverage. For instance, a usual coverage on a category consists of a set of covers, each of which comes with a target (the object it covers) and a set of morphisms (those in the cover). Thus, an internal coverage is an object $T$ of covers with maps $T\to C_0$ and $T \to P(C_1)$, where $C_0$ and $C_1$ are the objects and morphisms of the internal category. And so on. Strictly speaking, one doesn’t even need to do all this “by hand” – once we have the internal language of the topos developed, we just need to say “interpret the usual definition of coverage in the internal language”.

The occurrence of $P(-)$, the power-object functor, means that the definition as usually given only makes sense in an elementary topos. (This can be seen easily from the standard definition which says we have, for every object *a set* of covers, each consisting of *a set* of morphisms.) However, there are variants that make sense in pretoposes as well, which demand only a *family* of covers and a *family* of morphisms. What is more difficult in the latter situation is if one wants a notion of “sieve” and to demand that covering families consist of sieves.

The definition of internal site is obvious and straightforward.

Definition. For ℰ a topos, an internal site in ℰ is an internal category ℂ equipped with an internal coverage.

As far as I looked into the Elephant, the definition of *internal* coverage is to me very non-obvious, and, in particular, it is not clear to me wheather it is fully necessary to have a topos or it makes sense in somewhat more general categories. Do you have an insight which makes the complicated definition of *internal* coverage easier to comprehend and remember ?

now with a bit on the sheaf version

]]>started adding the discussion of externalization of internal sites. But only got to the presheaf case so far. Need to run now.

]]>stub for internal site. Hope to expand this later, but am out of time now.

Here is something I need to figure out in this context: over at the stub smooth super infinity-groupoid I thought better about what I should be doing there. I think I should take the idea that we are to be working over the base topos of sheaves over superpoints more seriously than I did so far.

Here is what I currently think one needs to do:

consider the base topos $Sh(SuperPoint)$ of presheaves on superpoints

this has a canonical line object $\mathcal{R} \in Sh(SuperPoint)$ which is such that the internal ordinary $\mathcal{R}$-linear algebra is externally traditional superalgebra.

Define an internal site $sCartSp$ whose objects are the $\mathcal{R}^n$s and whose morphisms are those morphisms in $Sh(SuperPoint)$ that are smooth according to the Schwarz-Molotkov-version of supermanifolds, as discussed there.

Then defined smooth super $\infty$-groupoids to be the internal $\infty$-sheaves on $sCartSp$.

I am beginning to think that this is the right way to go. But I need to understand better what this definition will unwind to in detail.

]]>