[Agda] Universe polymorphism in the standard library

Luke Palmer lrpalmer at gmail.com
Thu Nov 19 19:33:17 CET 2009


I have been diving into Agda recently, and have a decent amount of
tuits.  I notice that a decent amount of the standard library is not
using universe polymorphism.  Is there a reason for this, or is it
just that nobody has got a round tuit?  I'd be happy to start
converting things if the latter.

Luke


More information about the Agda mailing list