Commit 2024-05-10 13:12 fdad317e

View on Github →

chore(CategoryTheory/Sites): generalise universes and assumptions in CoverLifting file (#12798)

Estimated changes

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

modified def CategoryTheory.coherentTopology.equivalence'

modified def CategoryTheory.coherentTopology.equivalence

modified def CategoryTheory.regularTopology.equivalence

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

Modified Mathlib/Condensed/Equivalence.lean

modified def Condensed.ProfiniteCompHaus.equivalence

modified def Condensed.StoneanCompHaus.equivalence

modified def Condensed.StoneanProfinite.equivalence

modified theorem Condensed.isSheafProfinite

modified theorem Condensed.isSheafStonean

Modified Mathlib/Condensed/Explicit.lean