algebra.hierarchy_design

Stream: mathlib4

[Eric Rodriguez]

What should be done with this mostly-text file?

[Eric Rodriguez]

https://leanprover-community.github.io/mathlib_docs/algebra/hierarchy_design.html#library_note.the%20algebraic%20hierarchy for quick reference

[Kevin Buzzard]

I brought that file up at the porting meeting and the answer appeared to be "we have library notes so just port it"

[Eric Rodriguez]

the library design will surely be much different in Lean4, though

[Eric Rodriguez]

not now but after the port, anyways

[Eric Wieser]

Lots of things will change after the port, but that can't happen until the port has finished happening

[Eric Rodriguez]

mathlib4#657 is a crack at this. Please check my capitalistion!