[Agda] Universe construction

[David Haguenauer]

Hi list,

I'm trying to get a grasp of the ways in which Agda users program with
higher-level constructs than what the base language provides. It seems
to me as though universe construction was a hot topic in Agda-related
circles at some point in the past.

Are there any examples of significant developments making use of
universe construction? Or reasons why not?

-- 
Thanks,
David Haguenauer
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 254 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110111/c709017e/attachment.bin