Commit 2026-03-03 13:11 53113edf

feat(CategoryTheory/Sites): isomorphic hypercovers have equivalent sheaf conditions (#35901) More precisely, we show that if E and F are isomorphic 1-hypercovers, the associated multifork of E is exact if and only if the one for F is exact. Note that the same statement holds if E and F are homotopy equivalent, but, under mathlib's definition, for a general pre-1-hypercover E the identity refinement is not necessarily homotopic to itself.