title: What does "Error: Universe inconsistency" mean in Coq?
body: <p>I am working through <a href="http://www.cis.upenn.edu/~bcpierce/sf/current/" rel="noreferrer">Software Foundations</a> and am currently doing the exercises on Church numerals.  Here is the type signature of a natural number:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Definition nat := forall X : Type, (X -&gt; X) -&gt; X -&gt; X.
  </code></pre>
  
  <p>I have defined a function <code>succ</code> of type <code>nat -&gt; nat</code>.  I would now like to define an addition function like so:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Definition plus (n m : nat) : nat := n nat succ m.
  </code></pre>
  
  <p>However, I get the following error message:</p>
  
  <pre class="lang-coq prettyprint-override"><code>Error: Universe inconsistency.
  </code></pre>
  
  <p>What does this error message actually mean?</p>