这在纯属Agda中可证明，没有任何假设。解决方案是⊤ ≡ ⊥允许我们将⊤的任何证明转换为⊥的证明。

open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

theorem : ¬ (⊤ ≡ ⊥)
theorem eq = subst (λ A → A) eq tt

如果¬ ⊤ ≡ ⊥是¬ (⊤ ≡ ⊥)，则@Andras Kovacs为¬ ⊤ ≡ ⊥和¬ ⊥ ≡ ⊤都回答问题。如果¬ ⊤ ≡ ⊥是(¬ ⊤) ≡ ⊥，则证明要求类型相等。通常，只要证明¬ ⊤和⊥之间存在同构，就可以了。

(¬ ⊤) ≡ ⊥的证明表明¬ ⊤没有人居住。

然后，(¬ ⊥) ≡ ⊤的证明基本上证明了¬ ⊥仅具有一个功能id（因此对于包含单个元素的所有类型都是同构的）。

以下所有这些都可以使用一些标准的Agda函数来构造，但是这里需要证明这些同构的存在的自给自足的定义。注意False和True是类型，而不是布尔值。另外，由于¬ ⊥是一个函数，因此需要扩展性公理才能证明第二个定理。

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 \()

现在，如果我们为任意级别的类型Universe定义_==_，则可以引入有关类型相等的公理：如果两个类型具有同构性，则它们相等。

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