Solo estoy leyendo Tipos dependientes en el trabajo. En la introducción a los tipos parametrizados, el autor menciona que en esta declaración

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

el tipo deList esSet → Set y esoA se convierte en argumento implícito para ambos constructores, es decir.

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

Bueno, traté de reescribirlo un poco diferente

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

que lamentablemente no funciona (estoy tratando de aprender Agda durante dos días más o menos, pero por lo que deduje es porque los constructores están parametrizados sobreSet₀ y entoncesList A debe estar enSet₁).

De hecho, se acepta lo siguiente

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

sin embargo, ya no puedo usar{A : Set} → ... → List (List A) (que es perfectamente comprensible).

Entonces mi pregunta: ¿Cuál es la diferencia real entreList (A : Set) : Set yList : Set → Set?

¡Gracias por tu tiempo