なぜMonadはSet1のソートですか？

Question

私はAgdaのモナド型クラスをエンコードしようとしています。私はこれを遠くに持っています：

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 

だから、モナド「インスタンス」は実際に渡される関数の単なる記録です。質問：MonadのソートSet1はなぜですか？ Setとそれを注釈は、次のエラーを与える：

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 

私はMonadがSet1いうよりSetであると判断していくべきである何の思考プロセス？

Answer 1

アガはパラドックス（Russell's paradox,Hurkens' paradox）を防ぐために、無限のユニバーサル階層Set : Set1 : Set2 : ...を持っています。 _->_は、この階層を維持する：(Set -> Set) : Set1、(Set1 -> Set) : Set2、(Set -> Set2) : Set3、A -> B嘘はAとB嘘ユニバースに依存宇宙すなわち：A SさんがBよりも大きい "の場合、A -> BはAと同じ宇宙にある、そうでない場合はA -> BBと同じ宇宙にある。

あなたは（{A : Set}と{A B : Set}中）Set上を定量化しているが、それ故にreturnの種類とSet1で_⟫=_嘘は、それゆえ全体のことはSet1です。 Agda wikiで宇宙多型の

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 

より：明示的な宇宙でのコードは次のようになります。