Theorem CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq

Modification history

2026-03-03 13:11
Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean
feat(CategoryTheory/Sites): homotopy equivalent hypercovers have equivalent sheaf conditions (#35902) …
Modified CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eqView on Github →
2025-12-13 14:21
Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eqView on Github →
2025-09-11 17:39
Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean
chore(CategoryTheory/Sites): move `PreOneHypercover.Homotopy` in new file (#29553) …
Modified CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eqView on Github →
2025-06-28 10:39
Mathlib/CategoryTheory/Sites/OneHypercover.lean
feat(CategoryTheory/Sites): morphisms and homotopies of `1`-hypercovers (#26326) …
Added CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eqView on Github →