A coverage on a 2-category consists of, for each object , a collection of families of morphisms with codomain , called covering families, such that
A 2-category equipped with a coverage is called a 2-site.
If is a regular 2-category, then the collection of all singleton families , where is eso, forms a coverage called the regular coverage.
Likewise, if is a coherent 2-category, the collection of all finite jointly-eso families forms a coverage called the coherent coverage.
On , the canonical coverage consists of all families that are jointly essentially surjective on objects.
Let be a 2-site having finite limits (for convenience). For a covering family we have the comma objects
We also have the double comma objects with projections , , and .
Now, a functor is called a 2-presheaf. It is 1-separated if
It is 2-separated if it is 1-separated and
It is a 2-sheaf if it is 2-separated and
there exists an object and isomorphisms such that for all the following square commutes:
A 2-sheaf, especially on a 1-site, is frequently called a stack. However, this has the unfortunate consequence that a 3-sheaf is then called a 2-stack, and so on with the numbering all offset by one. Also, it can be helpful to use a new term because of the notable differences between 2-sheaves on 2-sites and 2-sheaves on 1-sites. The main novelty is that and need not be invertible.
Note, though, they must be invertible as soon as is (2,1)-site: by definition and since an inverse is provided by , where is the symmetry equivalence.
If lacks finite limits, then in the definitions of “2-separated” and “2-sheaf” instead of the comma objects , we need to use arbitrary objects equipped with maps , , and a 2-cell . We leave the precise definition to the reader.
A 2-site is said to be subcanonical if for any , the representable functor is a 2-sheaf. When has finite limits, it is easy to verify that this is true precisely when every covering family is a (necessarily pullback-stable) quotient of its kernel 2-polycongruence. In particular, the regular coverage on a regular 2-category is subcanonical, as is the coherent coverage on a coherent 2-category.
The 2-category of 2-sheaves on a small 2-site is, by definition, a Grothendieck 2-topos.
A pre-Grothendieck coverage on a 2-category is a coverage satisfying the following additional conditions:
If is an equivalence, then the one-element family is a covering family.
If is a covering family and for each , so is , then is also a covering family.
This is the 2-categorical version of a Grothendieck pretopology.
Now, a sieve on an object is defined to be a functor with a transformation which is objectwise fully faithful (equivalently, it is ff in ). Every family generates a sieve by defining to be the full subcategory of on those such that for some and some . The following observation is due to StreetCBS.
A 2-presheaf is a 2-sheaf for a covering family if and only if
is an equivalence, where is the sieve on generated by .
Therefore, just as in the 1-categorical case, it is natural to restrict attention to covering sieves. We define a Grothendieck coverage on a 2-category to consist of, for each object , a collection of sieves on called covering sieves, such that
If is a covering sieve on and is any morphism, then is a covering sieve on .
For each the sieve consisting of all morphisms into (the sieve generated by the singleton family ) is a covering sieve.
If is a covering sieve on and is an arbitrary sieve on such that for each in , is a covering sieve on , then is also a covering sieve on .
Here if is a sieve on and is a morphism, denotes the sieve on consisting of all morphisms into such that factors, up to isomorphism, through some morphism in .
As in the 1-categorical case, one can then show that every coverage generates a unique Grothendieck coverage having the same 2-sheaves.