Commit 2026-06-23 22:34 5cbb508e

View on Github →

chore(CategoryTheory/Sites): fix order of universe variables in Presieve.ofArrows_pUnit (#40974) The free universe variable should be the first one in the declaration, not the third.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/Fpqc.lean

Modified Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean

Modified Mathlib/CategoryTheory/Sites/MorphismProperty.lean

Modified Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

modified theorem CategoryTheory.Presieve.ofArrows_pUnit