Tipi induttivi parametrizzati in AGDA

Question

Sto solo leggendo Tipi dipendenti al lavoro. Nell'introduzione ai tipi parametrizzati, l'autore menziona che in questa dichiarazione

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

il tipo di List è Set → Set e quello A diventa argomento implicito ad entrambi i costruttori, cioè.

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

Bene, ho provato a riscriverlo in modo leggermente diverso

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

Il che purtroppo non funziona (sto cercando di imparare l'AGDA per circa due giorni, ma da quello che ho raccolto è perché i costruttori sono parametrizzati Set₀ e così List A deve essere dentro Set₁).

In effetti, quanto segue è accettato

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

Tuttavia, non sono più in grado di usare {A : Set} → ... → List (List A) (che è perfettamente comprensibile).

Quindi la mia domanda: qual è la differenza reale tra List (A : Set) : Set e List : Set → Set?

Grazie per il tuo tempo!