Commit 2020-06-30 04:15 1588d81eView on Github →
feat(category_theory): remove nearly all universe annotations (#3221)
Due to some recent changes to mathlib (does someone know the relevant versions/commits?) most of the universe annotations
include 𝒞 statements that were previously needed in the category_theory library are no longer necessary.
This PR removes them!