Adapt and use HB to generate Trocq relational structures

[CohenCyril]

Right now we cannot use HB for two reasons:

1. We rely crucially on universe polymorphism (trocq records have trocq records as their fields), and HB does not support it
2. We have serveral instances on the same type: e.g. Type has 36 different interpretations, and constants might be translated to themselves, or to custom targets.

However using HB already handles the gradual construction of records and could handle the symmetrisation easily, thus solving issue #24.

Another advantage of HB is that we could extend the Trocq hierarchy more easily and link it with that of functions (from e.g. https://github.com/math-comp/analysis/blob/master/classical/functions.v) and morphisms (from e.g. https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v)