title: How to write a type signature with two parameters?
body: <p>I try to learn agda and use the <a href="https://people.inf.elte.hu/divip/AgdaTutorial/Sets.Parametric.html#1" rel="nofollow noreferrer">tutorial</a>.
  I paste code for two mutally recursive sets</p>
  <pre><code>module MoreSets where 
  
  data List₁ (A B : Set) : Set
  data List₂ (A B : Set) : Set
  
  data List₁ (A B : Set) where
    []  :                 List₁ A B
    _∷_ : A → List₂ A B → List₁ A B
  
  data List₂ (A B : Set) where
    _∷_ : B → List₁ A B → List₂ A B
  </code></pre>
  <p>and get the error</p>
  <pre><code>MoreSets.agda:6,12-23
  Unexpected type signature for parameters A B
  when checking the definition of List₁
  </code></pre>
  <p>I assume a trivial error but cannot see it.</p>
  <p>What is a simple tutorial to learn agda for a Haskell programmer which does not go deep into category theory?</p>