Cantor's diagonal argument (sort of)

cantor.agda

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma

data ⊥ : Set where

¬_ : Set → Set
¬ P = P → ⊥

Surjective : {A B : Set} → (A → B) → Set
Surjective f = ∀ y → Σ _ λ x → f x ≡ y

Countable : Set → Set
Countable A = Σ (ℕ → A) Surjective

baire-uncountable : ¬(Countable (ℕ → ℕ))
baire-uncountable (f , sur) with sur λ n → suc (f n n)
baire-uncountable (f , sur) | x , fx≡ω = n≢sn (eqext fx≡ω x)
  where
    n≢sn : ∀{n} → ¬(n ≡ (suc n))
    n≢sn ()
    eqext : {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
    eqext refl x = refl