mathlib

18246ac4 - refactor(category_theory/finite_limits): reorganise import hierarchy (#3320)

refactor(category_theory/finite_limits): reorganise import hierarchy (#3320) Previously, all of the "special shapes" that happened to be finite imported `category_theory.limits.shapes.finite_limits`. Now it's the other way round, which I think ends up being cleaner. This also results in some significant reductions to the dependency graph (e.g. talking about homology of complexes no longer requires compiling `data.fintype.basic` and all its antecedents). No actual content, just moving content around. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>