Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures.
Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy.
A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](https://arxiv.org/abs/1102.1323).
Coq offers two mechanism that are suited to solve this task: typeclasses and canonical structures.
Both can be instrumented in different ways to obtain a (more or less) convenient-to-use algebraic hierarchy.
A common approach using typeclasses is the ["unbundled" approach by Bas Spitters and Eelis van der Weegen](https://arxiv.org/abs/1102.1323).