On `Set`-based rewriting of `Rel`

Stream: mathlib4

[SnO2WMaN]

I updated to mathlib tagged v4.22.0-rc4, I noticed Rel is rewrited to Set (α × β).
In our project, for useful, i was defined supplementary homogeneous relation HRel as Rel α α and use ReflGen, TransGen, and IsTrans, etc (See). But current mathlib's Rel definition is not suitable. What I want to know is whether you plan to rewrite ReflGen and other defs to make them suitable, or not in the future?

[Ruben Van de Velde]

Cc @Yaël Dillies

[Yaël Dillies]

I have no such plans

[Eric Wieser]

I think such changes would be a bad idea, too