Commit 2023-08-06 22:44 44692e22

View on Github →

chore: more universe generalisations / fixes (#5659) There are changes of two types: first I add some .{w} in some declarations to ensure that universes are in the right order. Secondly I generalise some results from Category.{max u1 v1, u2} to Category.{v2, u2}. From the Copenhagen workshop.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

modified def CategoryTheory.Limits.Multicofork.ofπ

modified def CategoryTheory.Limits.Multifork.ofι

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

modified def CategoryTheory.Presheaf.IsSheaf.amalgamate

modified theorem CategoryTheory.Presheaf.IsSheaf.amalgamate_map

modified theorem CategoryTheory.Presheaf.IsSheaf.hom_ext

modified theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf'

modified theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget

Modified Mathlib/CategoryTheory/Sites/Whiskering.lean