English
There is a natural equivalence between the IsLimit of opensLeCover generated cones and the IsLimit of pairwise generated cones.
Русский
Существует естественная эквивалентность между IsLimit открытых покрытий и IsLimit парных породившихся конусов.
LaTeX
$$$\text{isSheaf_iff_isSheafOpensLeCover} : F.IsSheaf \iff F.IsSheafOpensLeCover$$$
Lean4
instance (V : OpensLeCover U) : Nonempty (StructuredArrow V (pairwiseToOpensLeCover U)) :=
⟨@StructuredArrow.mk _ _ _ _ _ (single V.index) _ V.homToIndex⟩
-- This is a case bash: for each pair of types of objects in `Pairwise ι`,
-- we have to explicitly construct a zigzag.
