Theorem CategoryTheory.PreOneHypercover.sieve₀_cylinder

Modification history

2025-09-11 17:39

Mathlib/CategoryTheory/Sites/Hypercover/Homotopy.lean

chore(CategoryTheory/Sites): move `PreOneHypercover.Homotopy` in new file (#29553) …

Modified CategoryTheory.PreOneHypercover.sieve₀_cylinder View 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.sieve₀_cylinder View on Github →