Commit 2024-06-24 08:03 7788d14a

feat(CategoryTheory/Sites): the topology is generated by 1-hypercovers (#13011) In this PR, we show that a Grothendieck topology on a category C (with C : Type u and [Category.{v} C]) is (obviously) generated by 1-hypercovers of size max u v. In order to facilitate this, the type Cover.Relation is repackaged in a slightly different manner. Some proofs have been cleaned up. Several dsimp lemmas which had been manually added have been removed (and replaced by auto-generated ones).