Commit 2024-05-15 16:06 7926a8b7

feat(CategoryTheory/Sites): 1-hypercovers (#12803) This PR defines a notion of 1-hypercovers in a category C equipped with a Grothendieck topology J. A covering of an object S : C consists of a family of maps f i : X i ⟶ S which generates a covering sieve. In the favourable case where the fibre products of X i and X j over S exist, the data of a 1-hypercover consists of the data of objects Y j which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. If F is a sheaf and E is a 1-hypercover of S, we show that F.val.obj (op S) is a multiequalizer of suitable maps F.val.obj (op (X i)) ⟶ F.val.obj (op (Y j)).