  Abstract algebra provides a large hierarchy of properties that a collection
of objects can satisfy, such as forming an abelian group or a semiring. These
classifications can arranged into a broad and typically acyclic directed graph.
This graph perspective encodes naturally in the typeclass system of theorem
provers such as Lean, where nodes can be represented as structures (or records)
containing the requisite axioms. This design inevitably needs some form of
multiple inheritance; a ring is both a semiring and an abelian group.
  In the presence of dependently-typed typeclasses that themselves consume
typeclasses as type-parameters, such as a vector space typeclass which assumes
the presence of an existing additive structure, the implementation details of
structure multiple inheritance matter. The type of the outer typeclass is
influenced by the path taken to resolve the typeclasses it consumes. Unless all
possible paths are considered judgmentally equal, this is a recipe for
disaster.
  This paper provides a concrete explanation of how these situations arise
(reduced from real examples in mathlib), compares implementation approaches for
multiple inheritance by whether judgmental equality is preserved, and outlines
solutions (notably: kernel support for $\eta$-reduction of structures) to the
problems discovered.
