Commit 2025-06-28 10:39 255112e7

feat(CategoryTheory/Sites): morphisms and homotopies of 1-hypercovers (#26326) We define refinement morphisms and homotopies between morphisms of (pre-)-1-hypercovers. As a sanity check, we show that

• homotopic maps induce the same map on the corresponding multiequalizers
• the category of 1-hypercovers is cofiltered up to homotopies, i.e. for any two refinement morphisms there exists a refinement from the left such that both compositions are homotopic. In the next PR, we define the (homotopy) category of 1-hypercovers with refinement morphisms modulo homotopy. This will be a cofiltered category and taking a colimit over these will give a second approach to sheafification.