mathlib
bfd53845 - chore(category_theory): switch ulift and filtered in import hierarchy (#13302)

Commit
3 years ago
chore(category_theory): switch ulift and filtered in import hierarchy (#13302) Many files require `ulift` but not `filtered`, so `ulift` should be lower in the import hierarchy. This avoids needing all of `data/` up to `data/fintype/basic` before we can start defining categorical limits. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading