-- A formalization of Cantor's diagonal argument.

module Diag where

-- The empty/false type
data ⊥ : Set where

-- Negation of types. A type A is uninhabited if it entails
-- the empty type above.
infix 30 ¬_
¬_ : Set → Set
¬ A = A → ⊥

-- Dependent sums. Also function as existential quantifiers.
data Σ (A : Set) (P : A → Set) : Set where
  _,_ : (x : A) (w : P x) → Σ A P

-- Homogeneous built-in equality.
infix 40 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

infix 40 _≢_
_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬ x ≡ y

data Bool : Set where
  false : Bool
  true  : Bool

not : Bool → Bool
not false = true
not true  = false

-- Booleans are not equal to their negation. () is the absurd
-- pattern, which matches if the type checker judges a type to
-- not be inhabited. Here, they match 'false ≡ true' and
-- 'true ≡ false' respectively.
not-≢ : ∀ b → not b ≢ b
not-≢ true  ()
not-≢ false ()

-- The natural numbers.
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

-- If two functions are equal, then they agree on all elements.
lemma₀ : ∀{A B} → (f g : A → B) → f ≡ g → ∀ x → f x ≡ g x
lemma₀ .g g refl _ = refl

-- If there exists an element of the domain on which two functions
-- do not agree, then those two functions are not equal.
lemma₁ : ∀{A B} → (f g : A → B) → Σ A (λ x → f x ≢ g x) → f ≢ g
lemma₁ f g (x , fx≢gx) f≡g = fx≢gx (lemma₀ f g f≡g x)

-- Given any function b from the natural numbers to the 'power set'
-- of the naturals, as represented by functions ℕ → Bool, there
-- exists a 'set' f that is not in the image of b.
--
-- One might argue that ℕ → Bool isn't really a power set, because
-- there are countably many Agda functions, when we reason about
-- Agda in some meta-theory (since all Agda functions can be written
-- as finite strings of symbols). But, from the internal perspective,
-- ℕ → Bool looks uncountable. In other words, it's computably
-- uncountable. (I believe you'd have similar oddities doing model
-- theory on, say, ZF, where you can show that it has countable
-- models, but you can prove in ZF that various sets are uncountable.)
--
-- The classical mathematical proof obviously follows the same form.
-- And of course, the set of functions from A to B is often denoted
-- A^B, and one might denote the 2-element boolean set as 2, making
-- the function space 2^ℕ.
cantor : (b : ℕ → (ℕ → Bool)) → Σ (ℕ → Bool) (λ f → ∀ n → f ≢ b n)
cantor b = diag , diag≢bn
 where
 diag : ℕ → Bool
 diag n = not (b n n)

 diag≢bn : ∀ n → diag ≢ b n
 diag≢bn n = lemma₁ diag (b n) (n , not-≢ (b n n))