Commit 2020-06-30 04:15 1588d81e

View 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 .{v} and include 𝒞 statements that were previously needed in the category_theory library are no longer necessary. This PR removes them!

Estimated changes