§ Encoding mathematical hieararchies

I've wanted to learn how the SageMATH system is organized when it comes to math hieararchies. I also wish to learn how lean4 encodes their hiearchies. I know how mathematical components does it. This might help narrow in on what what the "goldilocks zone" is for typeclass design.

§ References