An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as is_sheaf_iff_is_sheaf_pairwise_intersections).

A presheaf is a sheaf if F sends the cone (pairwise.cocone U).op to a limit cone. (Recall pairwise.cocone U has cone point supr U, mapping down to the U i and the U i ⊓ U j.)

An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections).

A presheaf is a sheaf if F preserves the limit of pairwise.diagram U. (Recall pairwise.diagram U is the diagram consisting of the pairwise intersections U i ⊓ U j mapping into the open sets U i. This diagram has limit supr U.)

Implementation detail: the object level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U

Implementation detail: the morphism level of pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U

The category of single and double intersections of the U i maps into the category of open sets below some U i.

The diagram consisting of the U i and U i ⊓ U j is cofinal in the diagram of all opens contained in some U i.

The diagram in opens X indexed by pairwise intersections from U is isomorphic (in fact, equal) to the diagram factored through opens_le_cover U.

For a sheaf F, F(U ⊔ V) is the pullback of F(U) ⟶ F(U ⊓ V) and F(V) ⟶ F(U ⊓ V). This is the pullback cone.