Diagonal.agda

module Diagonal where

{-
demonstration of Cantor's diagonal argument
we prove that infinite sequences of bits are uncountable
-}

data 𝟚 : Set where
  O I : 𝟚

flip : 𝟚 → 𝟚
flip O = I
flip I = O

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

≡-trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans refl eq = eq

ap : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
ap f refl = refl

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

infix 15 _∎

_∎ : {A : Set} (x : A) → x ≡ x
x ∎ = refl

infixr 2 _⟨_⟩≡_

_⟨_⟩≡_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ⟨ eq ⟩≡ y=z = ≡-trans eq y=z

record _≅_ (A B : Set) : Set where
  constructor mk-≅
  field
    f : A → B
    g : B → A
    f∘g=x : ∀ {x} → f (g x) ≡ x
    g∘f=x : ∀ {x} → g (f x) ≡ x -- we don't even need this

data ⊥ : Set where

module Wrong (equiv : ℕ ≅ (ℕ → 𝟚)) where
  open _≅_ equiv
  
  dia : ℕ → 𝟚
  dia n = flip (f n n)

  dia-n : ℕ
  dia-n = g dia

  dia′ : ℕ → 𝟚
  dia′ = f dia-n

  -- note how we don't need this for agda proof, this is just illustration for readers
  -- because actual proof doesn't look especially easy to understand
  flipped-bit : dia dia-n ≡ flip (dia′ dia-n)
  flipped-bit =
    dia dia-n
      ⟨ refl ⟩≡
    flip (f dia-n dia-n)
      ⟨ ap flip refl ⟩≡
    flip (dia′ dia-n) ∎

  -- this is hard to read, but basic idea is that we observe what (dia′ dia-n) normalizes into.
  -- if O = (dia′ dia-n) = f (g dia) (g dia), then (dia dia-n) = flip (f (g dia) (g dia)) should
  -- be I and thus eq cannot be true, and vice versa
  wrong-bit : dia dia-n ≡ dia′ dia-n → ⊥
  wrong-bit eq with dia′ dia-n
  wrong-bit () | O
  wrong-bit () | I

  contradiction : ⊥
  contradiction = wrong-bit (ap (λ f → f dia-n) (sym f∘g=x))