Why is Monad of sort Set1?

Question

I've been trying to encode the Monad typeclass in Agda. I've gotten this far:

module Monad where
  record Monad (M : Set → Set) : Set1 where
    field
      return : {A : Set} → A → M A
      _⟫=_ : {A B : Set} → M A → (A → M B) → M B

So a Monad 'instance' is really just a record of functions that gets passed around. Question: Why is Monad of sort Set1? Annotating it with Set gives the following error:

The type of the constructor does not fit in the sort of the
datatype, since Set₁ is not less or equal than Set
when checking the definition of Monad

What thought process should I be going through to determine that Monad is Set1 rather than Set?

Answer 1

Agda has an infinite hierarchy of universes Set : Set1 : Set2 : ... to prevent paradoxes (Russell's paradox, Hurkens' paradox). _->_ preserves this hierarchy: (Set -> Set) : Set1, (Set1 -> Set) : Set2, (Set -> Set2) : Set3, i.e. the universe where A -> B lies depends on the universes where A and B lie: if A's is bigger than B's, then A -> B lies in the same universe as A, otherwise A -> B lies in the same universe as B.

You're quantifying over Set (in {A : Set} and {A B : Set}), hence the types of return and _⟫=_ lie in Set1, hence the whole thing lies in Set1. With explicit universes the code looks like this:

TReturn : (Set → Set) → Set1
TReturn M = {A : Set} → A → M A

TBind : (Set → Set) → Set1
TBind M = {A B : Set} → M A → (A → M B) → M B

module Monad where
  record Monad (M : Set → Set) : Set1 where
    field
      return : TReturn M
      _⟫=_ : TBind M

More on universe polymorphism in Agda wiki.