How to prove `theorem : ¬ ⊤ ≡ ⊥` in Agda?

Question

Following The Haskell Road to Logic, Maths and Programming, one can find p.48 Theorem 2.12.1 ¬ ⊤ ≡ ⊥ and its converse ¬ ⊥ ≡ ⊤

The book uses Haskell and assumes

1. ⊥ = False
2. ⊤ = True

which would yield the Agda type theorem : (p q : Bool) → not p ≡ q which is trivial to prove via refl.

However, can one prove the original theorem without assuming 1 and 2?

trying

-- from software foundations (https://plfa.github.io/Negation/)
postulate
  excluded-middle : ∀ {A : Set} → A ⊎ ¬ A

theorem : ¬ ⊤ ≡ ⊥
theorem x = {!!}

of course yields no solution, since we can't construct ⊥, 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?

Agda says:

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 ⊥

Thanks!

Answer 1

If ¬ ⊤ ≡ ⊥ is ¬ (⊤ ≡ ⊥), then @Andras Kovacs answer suits for both ¬ ⊤ ≡ ⊥ and ¬ ⊥ ≡ ⊤. If ¬ ⊤ ≡ ⊥ is (¬ ⊤) ≡ ⊥, then the proof requires an equality of types. Usually you should be fine with the proof of existence of isomorphism between ¬ ⊤ and ⊥.

The proof for (¬ ⊤) ≡ ⊥ establishes that ¬ ⊤ is not inhabited.

The proof for (¬ ⊥) ≡ ⊤ then essentially establishes the fact that ¬ ⊥ has only one function, id (hence is isomorphic to all types containing a single element).

All of the following can be constructed using some standard Agda functions, but here the self-sufficient bunch of definitions needed to prove the existence of such isomorphisms. Note False and True are types, not boolean values. Also, extensionality axiom is needed to be able to prove the second theorem, because ¬ ⊥ is a function.

data False : Set where

data True : Set where
  tt : True

data _==_ {A : Set} (x : A) : A -> Set where
   refl : x == x

false-elim : {A : Set} -> False -> A
false-elim ()

id : {A : Set} -> A -> A
id x = x

const : {A B : Set} -> B -> A -> B
const x _ = x

ap : {A B : Set} -> (A -> B) -> A -> B
ap = id

ap' : {A B : Set} -> A -> (A -> B) -> B
ap' x f = f x

infixl 4 _==_

data Isomorphism {A B : Set} (f : A -> B) (g : B -> A) : Set where
   iso : ((x : B) -> f (g x) == id x) ->
         ((x : A) -> g (f x) == id x) -> Isomorphism f g

Not : Set -> Set
Not A = A -> False

not-True-iso-False : Isomorphism (ap' tt) false-elim
not-True-iso-False = iso (\x -> false-elim {ap' tt (false-elim x) == id x} x)
                         \not-true -> false-elim (not-true tt)

-- extensionality: if functions produce equal results for all inputs, then the functions are equal
postulate ext : {A B : Set} -> (f g : A -> B) -> ((x : A) -> f x == g x) -> f == g

not-False-iso-True : Isomorphism {Not False} {True} (const tt) (const id)
not-False-iso-True = iso is-true is-not-false where
   is-true : (x : True) -> const tt (const {True} (id {Not False})) == id x
   is-true tt = refl
   is-not-false : (x : Not False) -> const id (const {Not False} tt) == id x
   is-not-false x = ext (const id (const {Not False} tt)) x \()

---

Now, if we define _==_ for any level of type universe, then we can introduce the axiom about type equality: if two types have an isomporphism, then they are equal.

open import Agda.Primitive
data _==_ {a : Level} {A : Set a} (x : A) : A -> Set a where
   refl : x == x

postulate iso-is-eq : {A B : Set} {f : A -> B} {g : B -> A} ->
                      Isomorphism f g -> A == B

not-True-is-False : (Not True) == False
not-True-is-False = iso-is-eq not-True-iso-False

not-False-is-True : (Not False) == True
not-False-is-True = iso-is-eq not-False-iso-True