Параметризованные индуктивные типы в Agda

Я только что читаю Зависимые типы в действии .Во введении к параметризованным типам автор упоминает, что в этом объявлении

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List A

типом List является Set → Set и что A становится неявным аргументом для оба конструктора, т.е.

[]   : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A

Ну, я попытался переписать его немного по-другому

data List : Set → Set where
  []   : {A : Set} → List A
  _::_ : {A : Set} → A → List A → List A

, что, к сожалению, не работает (я пытаюсь изучить Agda в течение двух дней или около того, но из того, что я понял, это потому, что конструкторы параметризованы по ] Set₀ и поэтому Список A должен быть в Set₁ ).

Действительно, следующее принято

data List : Set₀ → Set₁ where
  []   : {A : Set₀} → List A
  _::_ : {A : Set₀} → A → List A → List A

, однако я больше не могу использовать {A: Set} → ... → List (List A) (что совершенно понятно).

Итак, мой вопрос: в чем разница между List (A: Set): Set и List: Set → Set ?

Спасибо за ваше время!