feat(CategoryTheory/Sites): characterization of sheaves using 1-hypercovers

[joelriou]

In this PR, given a Grothendieck topology J on a category C, we define a type J.OneHypercoverFamily of families of 1-hypercovers. When H : J.OneHypercoverFamily, we define a predicate H.IsGenerating which means that any covering sieve contains the sieve generated by the underlying covering of one of the 1-hypercovers in the family. If this holds, we show in OneHypercoverFamily.isSheaf_iff that a presheaf P : Cᵒᵖ ⥤ A is a sheaf iff for any 1-hypercover E in the family, the multifork E.multifork P is limit.

---