Commit 2020-07-08 08:25 18246ac4

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.