mathlib
8e8037f5 - chore(category_theory/limits): remove dependency on concrete_categories (#2411)

Commit
5 years ago
chore(category_theory/limits): remove dependency on concrete_categories (#2411) Just move some content around, so that `category_theory/limits/cones.lean` doesn't need to depend on the development of `concrete_category`. Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Author
Parents
Loading