N≠Bool.agda

-- In type theory we can show that ℕ and Bool are not equal as follows

module N≠Bool where

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Bool
open import Data.Sum
open import Data.Empty

-- The definition of an injective map

injective : {A B : Set} (f : A → B) → Set
injective f = ∀ {x y} → f x ≡ f y → x ≡ y

-- Among three boolean values two are equal

three-bool : ∀ (a b c : Bool) → a ≡ b ⊎ a ≡ c ⊎ b ≡ c
three-bool false false _ = inj₁ refl
three-bool true true _ = inj₁ refl
three-bool false true false = inj₂ (inj₁ refl)
three-bool false true true = inj₂ (inj₂ refl)
three-bool true false false = inj₂ (inj₂ refl)
three-bool true false true = inj₂ (inj₁ refl)

-- The numbers 0, 1 and 2 are distinct

0≠1 : 0 ≡ 1 → ⊥
0≠1 ()

0≠2 : 0 ≡ 2 → ⊥
0≠2 ()

1≠2 : 1 ≡ 2 → ⊥
1≠2 ()

-- There is no injective map f : ℕ → Bool because two of
-- f 0, f 1 and f 2 have to be equal

no-injective : ∀ (f : ℕ → Bool) → injective f → ⊥
no-injective f injective-f with three-bool (f 0) (f 1) (f 2)
... | inj₁ p = 0≠1 (injective-f p)
... | inj₂ (inj₁ p) = 0≠2 (injective-f p)
... | inj₂ (inj₂ p) = 1≠2 (injective-f p)

-- There is an injection between any two equal types

ι : ∀ {A B : Set} → A ≡ B → A → B
ι refl x = x

injective-ι : ∀ {A B} (p : A ≡ B) → injective (ι p)
injective-ι refl refl = refl

-- If ℕ and Bool were equal, we would have an injection
-- from ℕ to Bool, but we do not.

ℕ≠Bool : ℕ ≡ Bool → ⊥
ℕ≠Bool p = no-injective (ι p) (injective-ι p)