A coverage, named t, on the category k. Several coverages can live on one category, so the name is a parameter rather than a wrapper on the kind.

A cover is given by its legs, the generating arrows of the covering family. The identity cover, which every coverage has, is left implicit: Cover and covers list the others. The one law is

Stability

covers pull back. Given a cover c of a and any f :: b ~> a, the object b has a cover -- possibly just its identity -- each of whose legs h satisfies f . h = legArrow g . h' for some leg g of c and some h'. Only the equation is asked for; no pullback object has to exist.

A leg of the cover c of a, with its source hidden.

A site whose covers can be listed, object by object. This is what the law tests and the decision procedure of Proarrow.Category.Enriched.Finitary.Sheaf quantify over. A free category is a Site but not this: whether an object is a sum is not something its Ob can answer.

Beyond Site's Stability, listing the covers comes with a second law:

Composition

covers compose. If c covers a and every leg of c is itself covered, the composites cover a too. Stability and composition together are what make the coverage generate a Grothendieck topology, and so make closure idempotent and meet-preserving -- without which the dense sieves at an object are not closed under meets, which is what Plus rests on. testLawvereTierney is the check.

A cover of a, with its name hidden.

A profunctor that is a sheaf for the coverage t on the contravariant side: elements over a cover glue. A family m over the legs of a cover c is matching when it agrees on overlaps: for legs g and g' and any p :: z ~> x, q :: z ~> y with legArrow g . p = legArrow g' . q, lmap p (m g) = lmap q (m g'). Sums below is the smallest worked instance of that condition, where it comes to one equation. The laws are

Restriction

for matching m, lmap (legArrow g) (glue c m) = m g at every leg g of c: the gluing restricts back to the family;

Uniqueness

glue c (\g -> lmap (legArrow g) x) = x: an element is the gluing of its own restrictions.

The laws constrain glue on matching families only, and its type accepts any family, so its value on a non-matching one is unspecified. The Sums instance below is the live example: it keeps one leg's covariant component and discards the other, which is sound only because matching forces them equal.

Together they say that restriction is a bijection from the elements at a to the matching families on c, which is the sheaf condition. Gluing is stated for every b at once: a profunctor j +-> k is a sheaf when, for each object b of j, the presheaf p (-) b on k is one. Once the glued element at (a, b) is fixed, dimap fixes its value at every other point (g, h) of the sieve the cover generates -- which is why Proarrow.Category.Enriched.Finitary.Sheaf can decide the same condition as natural transformations out of that sieve.

Gluing is contravariant, and not by choice: a coverage presents each object by the arrows into it, and k is the side of p a b that lmap acts on. The dual needs a cocoverage, which is a coverage on OPPOSITE k, and a cosheaf for it is Sheaf t (Op p); nothing supplies a cocoverage yet, though Finitary (Op p) makes the machinery available for one. The instances are indexed by the shape of the profunctor: the limits just below, a site's representables, and the image of sheafification (Plus twice over). One indexed by the coverage instead cuts across that axis and so overlaps all of them -- which is why glueTrivial is a function and not an instance Sheaf Trivial p.

The trivial coverage: only identities cover, so every profunctor is a sheaf.

Every profunctor is a sheaf for Trivial, by the eliminator of an empty Cover. This is a function rather than an instance Sheaf Trivial p because that head and the two closure instances above overlap -- at Sheaf Trivial TerminalProfunctor, say -- with neither more specific than the other, so GHC could not choose between them. Write glue = glueTrivial to get the instance for one profunctor.

The walking arrow BOOL with TRU covered by FLS alone. The one leg has no overlap with itself beyond its source, so every element at FLS is a matching family, and a presheaf is a sheaf exactly when its restriction along F2T is a bijection. The coverage is stable, since pulling the cover back along F2T gives the identity of FLS, but not subcanonical: the representable at FLS has an element at FLS and none at TRU, so it is not a sheaf.

The name of ByArrow's one cover, whose Cover constructor is TruByFls and whose one Leg constructor is ViaF2T.

The open-cover coverage of the discrete two-point space, whose opens are (BOOL, BOOL) (see Proarrow.Category.Instance.Product): the whole space is covered by its two singletons, and the empty set by no opens at all. The covers are stable and compose, so the covering sieves are exactly those whose union is the object; and since a union of opens is their colimit -- the empty union included -- every representable presheaf is a sheaf: the coverage is subcanonical. A sheaf has exactly one section over the empty set, and its sections over the whole space are the pairs of sections over the two points.

Subcanonical is about the representable presheaves. A two-sided Yo a (OP b) need not be a sheaf: the empty cover asks for exactly one element at '(FLS, FLS) for every object of j, while Yo a (OP b) has none at an object b has no arrow to.

The name of Canonical's cover of the whole space, whose Cover constructor is ByPoints and whose Leg constructors are AtX and AtY, one per singleton.

The name of Canonical's cover of the empty set, whose Cover constructor is ByNothing and which has no legs.

The sum coverage on a free category with binary coproducts: a sum is covered by its two injections. This is the syntactic site of Spiwack's post (see the module header) -- the free bicartesian closed category Syntax is one such category, with the booleans the sum TermF + TermF covered by true and false.

Read p a as the ways of producing a result of type a, and the module header's two failures become concrete: too many is two elements of p Bool with the same branches, so a proof by cases establishes nothing; too few is a pair of branches with no conditional, so if-then-else is not definable.

One caveat, and a real one: Site's Stability law does not hold for this coverage as declared. Covers live only at objects whose shape is syntactically x + y, so stability would need every arrow into a sum to decompose its domain -- that is extensivity, and a free bicartesian category is not extensive. Two witnesses: id ||| lft at (u + u) + u ~> u + u needs only coproducts, and its restriction to the left summand is id, which factors through neither injection; and with a richer constraint list mempty :: UnitF ~> u + u has a source that is not a sum at all, so no cover is even available. Nothing here breaks -- glue's laws below are the coproduct's universal property and need no stability, and FREE is deliberately not a HasFiniteCovers, so the topology machinery is never instantiated at it -- but this coverage does not generate a Grothendieck topology, and the licence that HasFiniteCovers's covers gives -- to check only the covers it lists -- does not extend to it.

Being a sheaf is exactly p Bool ≅ p TermF × p TermF: every pair of branches has a conditional, and only one. On a representable that conditional is |||, which is why glue below is [t, e]; the conditional on a test f :: c ~> Bool with branches over c is either, which needs the distributive law as well.

The free category cannot list the covers of an arbitrary object, so this is a Site and not a HasFiniteCovers.

The name of the cover of x + y by its injections, whose Cover constructor is BySummands and whose Leg constructors are AtLeft and AtRight.