title: Why can't (Set -> Set) have type Set?
body: <p>In Agda, the type of a <code>forall</code> is determined in such a way that the following all have type <code>Set1</code> (where <code>Set1</code> is the type of <code>Set</code> and <code>A</code> has type <code>Set</code>):</p>
  
  <pre><code>Set → A
  A → Set
  Set → Set
  </code></pre>
  
  <p>However, the following has type <code>Set</code>:</p>
  
  <pre><code>A → A
  </code></pre>
  
  <p>I understand that if <code>Set</code> had type <code>Set</code>, there would be contradictions, but I'm failing to see how, if any of the three terms above had type <code>Set</code>, we would have contradictions. Can those be used to prove False? Can they be used to show that <code>Set : Set</code>?</p>