The category of open sets contained in some element of the cover.

An arbitrarily chosen index such that V ≤ U i.

The morphism from V to U i for some i.

supr U as a cocone over the opens sets contained in some element of the cover.

(In fact this is a colimit cocone.)

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

A presheaf is a sheaf if F sends the cone (opens_le_cover_cocone U).op to a limit cone. (Recall opens_le_cover_cocone U, has cone point supr U, mapping down to any V which is contained in some U i.)

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.

The cocone pairwise.cocone U with cocone point supr U over pairwise.diagram U is isomorphic to the cocone opens_le_cover_cocone U (with the same cocone point) after appropriate whiskering and postcomposition.

The sheaf condition in terms of a limit diagram over all { V : opens X // ∃ i, V ≤ U i } is equivalent to the reformulation in terms of a limit diagram over U i and U i ⊓ U j.

The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of a limit diagram over all { V : opens X // ∃ i, V ≤ U i }.