Commit 2024-05-12 16:16 61fdb6c6

View on Github →

chore(CategoryTheory/Sites): generalise universes for extensive sheaves (#12801)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

modified theorem CategoryTheory.isSheaf_iff_preservesFiniteProducts

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

modified def CategoryTheory.Equalizer.Presieve.Arrows.FirstObj

modified def CategoryTheory.Equalizer.Presieve.Arrows.SecondObj

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

Modified Mathlib/Condensed/Explicit.lean