The sieve a cover generates at (a, b): the arrows into a that factor through a leg, paired with every arrow out of b.

Whether a sieve is the maximal one -- every arrow of the category is in it.

Whether every point of the second sieve is a point of the first.

Whether a sieve is covering: either it is the maximal sieve, or it contains the sieve that some cover of its object generates -- which, a sieve being closed under composition, is to contain that cover's legs (coveringCover).

That is the coverage taken at face value. It agrees with the Grothendieck topology the coverage generates only when the covers are stable and compose. When they do not, closure stops being idempotent, and testLawvereTierney is where that shows up.

The first listed cover all of whose legs lie in the sieve, if there is one. This is the search isCovering makes and the one extendPlus needs, and it needs no tabulation: whether a sieve contains the legs at the identity decides whether it contains everything they generate.

So it trusts the closure Proarrow.Profunctor.Instance.Sieve does not enforce: on a hand-built predicate that is not a sieve it says yes where comparing the whole generated sieve says no.

The Lawvere–Tierney closure of a sieve: the pairs (g, h) along which it pulls back to a covering one. A sieve is covering exactly when its closure is the maximal sieve.

Note both components -- dimap g h, not just lmap g. A coverage constrains only the contravariant side, but a sieve over j +-> k has two, which is why Props.Sheaf checks this function's naturality at a non-trivial j.

The coverage as a Lawvere–Tierney topology on the topos of finitary profunctors: closure, as an arrow on the subobject classifier.

Whether a finitary profunctor is a sheaf for the coverage: at every pair of objects and every cover, restriction is a bijection from the elements at the covered object to the matching families on the sieve the cover generates.

The sheaf condition at one cover: the restrictions of the elements at the covered object are exactly the matching families on the sieve it generates, as multisets.

Present a finitary profunctor by its tables, as withTabulated does, and tag the presentation with the coverage -- which is to give it a Sheaf instance. What that instance asserts is decided here, by isSheaf, so the assertion is backed by an enumeration and not by the caller's word; the failure continuation is taken when the profunctor is no sheaf for t.

This is how a sheaf with no Sheaf instance of its own -- a representable, a sheafification -- becomes an object of SHEAVES. It is also the cheap way to be one: the condition is decided on the tables rather than on p, where a Sheafify answers a single toIndex by re-running the whole plus construction.

A sieve as a subobject of the representable, handed on with its inclusion: the natural transformations out of that subobject are exactly the matching families on the sieve, with no separate treatment of the points outside it and no argument about which naturality conditions may be dropped. This is the one notion of matching family in the module; sheafAt and Plus both go through it.

withSubobject checks the closure a sieve must have, and its failure branch is unreachable for any coverage, lawful or not: generatedSieve's membership ignores its covariant argument and is closed under precomposition, and leastDenseSieve is a meet of sieves. Reaching it would take a Finitary instance on the hom-profunctor whose elements omits an arrow, which testFinitary rules out.

One step of the plus construction for the topology t. An element at (a, b) is a matching family on a dense sieve, taken up to agreement on a dense sieve; a Plus value holds one such family, as a partial function whose support is its sieve -- the sieve is never stored separately and so cannot disagree with the family. On a finite site whose coverage is a Grothendieck topology the dense sieves have a least one, leastDenseSieve, and every element has exactly one family on it: so the element a value stands for is its restriction to that sieve, plusTable, and that is what Finitary numbers and Proarrow.Testing compares. Nothing has to be quotiented.

That is HasFiniteCovers's Composition law, and leastDenseSieve fails loudly rather than compute where it does not hold.

The constructor checks none of: that the support is a sieve, that it is dense, that the family is matching -- as Sieve's does not check closure. plusElements builds only lawful values; one built by hand is its builder's responsibility.

The sieve a value is defined on.

Whether a sieve is dense for the topology: its closure is the maximal sieve. On a lawful coverage this agrees with isCovering -- testDenseIsCovering checks that -- but it is the stable notion, and Plus needs stability, since dimap pulls a support back along arrows.

The meet of all the dense sieves at a pair of objects, and so the least dense sieve -- when the covers compose, since that is what makes closure preserve meets. Restriction to it is what picks one matching family out of each element of Plus. On a coverage whose covers pull back but do not compose the meet need not be dense, and this errors, naming the law that failed, rather than let Plus compute on it: a poset w ≤ x ≤ a, w ≤ y ≤ a with a covered by x and by y separately and each of those by w is the smallest example.

The elements of Plus at a pair of objects: the matching families on the least dense sieve, in the order natElements lists them.

A value restricted to a sieve reified as a subobject: the natural transformation out of it that the value's family is.

A value's restriction to the least dense sieve, as its natTable: the indices of its values at that sieve's points. See Plus for what that determines.

Whether two values stand for the same element: their restrictions to the least dense sieve agree. One sieve for the pair, where two plusTables would each build their own -- which is what Proarrow.Testing's equality on Plus wants, since it compares far more often than it shows.

Sheafification: the plus construction twice. One Plus makes a profunctor separated -- two elements with the same restrictions to a dense sieve are equal -- and the second makes it a sheaf. The first alone need not: Props.Sheaf's constant presheaf on the two-point space has one section over the empty set after one plus, but still two over the whole space where a sheaf needs four. On a site whose covers have no overlaps, ByArrow say, one plus is already a sheaf and the second changes nothing.

The unit of the plus construction: an element as the family of its own restrictions, on the maximal sieve.

unitPlus twice: the unit of sheafification.

The universal property, one plus at a time: a map into a sheaf extends along unitPlus. A dense support either is everything, and the family is read off at the identity, or contains the legs of some listed cover -- that is what density at the identity says, and coveringCover finds it -- and the family restricted to those legs glues. Which cover is found does not matter, q being a sheaf; nor need q be Finitary -- gluing is all that is asked of it.

Gluing for the plus construction: a matching family over a cover, assembled into one family. At (g, h) it takes the first leg that g factors through and whose family is defined at the factor -- factorThrough gives that factor u, and the value is the leg's family at (u, h). So the support of the result is what the legs generate from the legs' own supports, which is dense by HasFiniteCovers's Composition law.

Well definedness -- that another leg, or another factorisation through the same leg, gives the same value -- is exactly what matching says, and glue is unconstrained on families that are not matching, so the first one found is as good as any.

extendPlus twice: a map into a sheaf extends along unitSheafify.

The full subcategory of FINITARY j k on the sheaves for t: the finitary profunctors that have a Sheaf instance. Its finite limits are computed exactly as FINITARY's and are sheaves by the closure instances -- TerminalProfunctor, :*:, and Reindex for the equalizers. Its colimits are not computed as FINITARY's: a quotient of sheaves is no sheaf, and they go through Sheafify. Its hom-sets are finitary by the conjunction instance in Proarrow.Category.Enriched.Finitary.Topos.

A sheaf as an object of SHEAVES, as FIN names an object of FINITARY.