[Agda] monad in Set

[Dan Licata]

Hi everyone,

Is there a way to describe the syntax of a monad, whose result type is
an arbitrary Agda Set, without using Set1?  E.g.

  data Comp (C : Set) : Set where
    Return : C -> Comp C
    Bind   : {A : Set} -> (A -> Comp C) -> (Comp A -> Comp C)

doesn't work because of the A argument to Bind.

-Dan