title: How to prove `theorem : ¬ ⊤ ≡ ⊥` in Agda?
body: <p>Following <em>The Haskell Road to Logic, Maths and Programming</em>, one can find p.48 <strong>Theorem 2.12.1</strong> <code>¬ ⊤ ≡ ⊥</code> and its converse <code>¬ ⊥ ≡ ⊤</code></p>
  
  <p>The book uses Haskell and assumes</p>
  
  <ol>
  <li><code>⊥ = False</code></li>
  <li><code>⊤ = True</code></li>
  </ol>
  
  <p>which would yield the Agda type <code>theorem : (p q : Bool) → not p  ≡ q</code> which is trivial to prove via <code>refl</code>.</p>
  
  <p>However, can one prove the original theorem without assuming 1 and 2?</p>
  
  <p>trying</p>
  
  <pre><code>-- from software foundations (https://plfa.github.io/Negation/)
  postulate
    excluded-middle : ∀ {A : Set} → A ⊎ ¬ A
  
  theorem : ¬ ⊤ ≡ ⊥
  theorem x = {!!}
  </code></pre>
  
  <p>of course yields no solution, since we can't construct <code>⊥</code>, so I guess a proof by contradiction is needed? Also, am I correct that this assumes the law of the excluded middle, which is therefore required as an additional postulate?</p>
  
  <p>Agda says:</p>
  
  <blockquote>
    <p>I'm not sure if there should be a case for the constructor refl,
    because I get stuck when trying to solve the following unification
    problems (inferred index ≟ expected index):
      ⊤ ≟ ⊥
    when checking that the expression ? has type ⊥</p>
  </blockquote>
  
  <p>Thanks!</p>