--- Day changed Sat Dec 30 2017
svercerpgiarrusso: how would that work (working up to 42)? There's no Level< type. AFAIK you can't write a universe-polymorphic type with a maximum level... so it's either a single fixed level or Set\omega. Unless there is a way, in which case that's exactly what I'm looking for. Also Set\omega isn't empty; it contains the type '\forall a -> Set a'... (in my idea Level would still just range over N, so that 30/12 01:30
svercerquantifier would still end up in Set\omega).30/12 01:30
svercerEduard_Munteanu: but that will end up searching for any instance method with the same signature, which might be too broad a search, yeah? Unless... maybe you wrap the result of the function in a unique-for-this-purpose record to make it distinct from others. But that rather takes the 'class' out of 'typeclass', doesn't it?30/12 01:33
pgiarrussosvercer: single-method typeclasses can be conceived, and exist in Coq, but then we’re30/12 02:28
pgiarrusso*were30/12 02:28
pgiarrussoSorry30/12 02:28
pgiarrussoWith single-method typeclasses, we’d be back to the same question: which universe would the record live in?30/12 02:29
pgiarrussosvercer: the way to get Level< is *cumulativity*, as available in Coq: each level includes previous ones. With cumulativity, all members of Set i, with i <= 42, would also be in Set 4230/12 02:30
pgiarrussoBut agda does not have cumulativity, which is a significant annoyance30/12 02:32
pgiarrussoI agree that Set \omega is not empty, what I wrote was nonsense30/12 02:33
heathGuy L Steele A Cobbler's Child https://www.youtube.com/watch?v=qNPlDnX6Mio30/12 03:15

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!