[Agda] set levels in Algebra.Structure

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Fri Jan 15 00:55:33 CET 2010


On 2010-01-14 12:38, Florent Balestrieri wrote:
> 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 ?

Yes: no one has generalised the code yet.

--
/NAD


More information about the Agda mailing list