Commit 2025-10-01 22:02 c6973413

feat(CategoryTheory/Sites): the category of 1-hypercovers up to homotopy (#29551) We define the category of 1-hypercovers up to homotopy as the category of 1-hypercovers where morphisms are considered up to existence of a homotopy. We show that this category is cofiltered if the base category has pullbacks. This category will be used to define a second construction of sheafification by taking certain colimits of multiequalizers over this category.