§ 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.