title: Parametrized Inductive Types in Agda
body: <p>I'm just reading <a href="http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf" rel="noreferrer"><em>Dependent Types at Work</em></a>. In the introduction to parametrised types, the author mentions that in this declaration</p>
  
  <pre><code>data List (A : Set) : Set where
    []   : List A
    _::_ : A → List A → List A
  </code></pre>
  
  <p>the type of <code>List</code> is <code>Set → Set</code> and that <code>A</code> becomes implicit argument to both constructors, ie.</p>
  
  <pre><code>[]   : {A : Set} → List A
  _::_ : {A : Set} → A → List A → List A
  </code></pre>
  
  <p>Well, I tried to rewrite it a bit differently</p>
  
  <pre><code>data List : Set → Set where
    []   : {A : Set} → List A
    _::_ : {A : Set} → A → List A → List A
  </code></pre>
  
  <p>which sadly doesn't work (I'm trying to learn Agda for two days or so, but from what I gathered it's because the constructors are parametrised over <code>Set₀</code> and so <code>List A</code> must be in <code>Set₁</code>).</p>
  
  <p>Indeed, the following is accepted</p>
  
  <pre><code>data List : Set₀ → Set₁ where
    []   : {A : Set₀} → List A
    _::_ : {A : Set₀} → A → List A → List A
  </code></pre>
  
  <p>however, I'm no longer able to use <code>{A : Set} → ... → List (List A)</code> (which is perfectly understandable).</p>
  
  <p>So my question: What is the actual difference between <code>List (A : Set) : Set</code> and <code>List : Set → Set</code>?</p>
  
  <p>Thanks for your time! </p>