A simple Agda proof that the set of naturals is infinite

NatIsInfinite.agda

open import Level using (_⊔_)
open import Function
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat hiding (_⊔_)
open import Data.Nat.Properties
open import Data.Vec
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Core

module NatIsInfinite where

-- Two sets are isomorphic when there is a bijection between them
record _≅_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  field
    to   : A → B
    from : B → A

    inverseˡ : to ∘ from ≗ id
    inverseʳ : id ≗ from ∘ to

-- A set is finite when it's isomorphic to Fin ℵ
record Finite {ℓ} (A : Set ℓ) : Set ℓ where
  field
    ℵ : ℕ
    iso : A ≅ Fin ℵ

-- Conversely, a set is infinite when it's not finite
Infinite : ∀ {ℓ} → Set ℓ → Set ℓ
Infinite A = ¬ Finite A

-- If a set is finite, we can put all its elements in a vector,
-- that we call a table
table : ∀ {ℓ} {A : Set ℓ} (finite : Finite A) → Vec A (Finite.ℵ finite)
table finite = tabulate from where open Finite finite; open _≅_ iso

-- All elements of a finite set are in its table
finite-table : ∀ {ℓ} {A : Set ℓ} (finite : Finite A) → ∀ a → a ∈ table finite
finite-table finite a
  with to a | inverseʳ a where open Finite finite; open _≅_ iso
...  | i    | a=from[i] rewrite a=from[i] = ∈-tabulate i
  where
    ∈-tabulate : ∀ {ℓ} {A : Set ℓ} {ℵ} {f : Fin ℵ → A} i → f i ∈ tabulate f
    ∈-tabulate zero = here
    ∈-tabulate (suc i) = there (∈-tabulate i)

-- Lemma: for an arbitrary vector of naturals we can find
-- a natural that is not in it
∃x∉xs : ∀ {n} (xs : Vec ℕ n) → ∃ λ x → ¬ x ∈ xs
∃x∉xs xs = suc (sum xs) , n≮n ∘ ≤-sum xs
  where
    n≮n : ∀ {n} → ¬ n < n
    n≮n (s≤s n<n) = n≮n n<n

    ≤-sum : ∀ {n} (xs : Vec ℕ n) → ∀ {x} → x ∈ xs → x ≤ sum xs
    ≤-sum (x ∷ xs) here = m≤m+n x (sum xs)
    ≤-sum (x ∷ xs) (there x∈xs) = ≤-steps x (≤-sum xs x∈xs)

-- The proof that the set of naturals is infinite
ℕ-infinite : Infinite ℕ
ℕ-infinite finite = contradiction
  where ∀n∈table = finite-table finite _
        ∃n∉table = ∃x∉xs _
        contradiction = proj₂ ∃n∉table ∀n∈table