[Agda] set levels in Algebra.Structure

[Florent Balestrieri]

Hello,
In lib-0.3, is there a reason why all equivalence relations which are 
record parameters  in the module Algebra.Structure are constrained to be 
in Set 0 ? it seems all the work in generalising the signatures using 
universe polymorphism in the Relation/* modules is ignored. Maybe it is 
an automatic source code transformation to keep Algebra.Structure 
compatible with the new interface (replacing `Rel A' with `Rel A 0') ?
-- Florent