[Agda] monad in Set

[Nils Anders Danielsson]

On 2009-06-17 13:05, Dan Licata wrote:
> 
> Is there a way to describe the syntax of a monad, whose result type is
> an arbitrary Agda Set, without using Set1?

Agda should really have support for some notion of universe
polymorphism... One workaround is to quantify over a small universe
instead of Set. You can also cheat by using --type-in-type. I usually
subject myself to the pain of working with a type in Set₁ (this explains
the existence of the various standard library modules with names ending
in "1").

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.