Commit 2024-01-16 02:11 d3bb4291

View on Github →

chore(CategoryTheory/Sites): universe polymorphic EqualizerCondition (#9729) Removes unnecessarily restrictive explicit universes

Estimated changes

Modified Mathlib/CategoryTheory/Sites/RegularExtensive.lean

modified theorem CategoryTheory.regularCoverage.EqualizerCondition.isSheaf_iff

modified def CategoryTheory.regularCoverage.EqualizerCondition

modified def CategoryTheory.regularCoverage.MapToEqualizer

modified theorem CategoryTheory.regularCoverage.equalizerCondition_of_regular

modified theorem CategoryTheory.regularCoverage.isSheaf_of_projective