A constructive proof that there is no largest natural number, from scratch.

4SWC.agda

-- A constructive proof that there is no biggest natural. I.e., we construct the
-- type "there is no biggest natural" and construct an element of it. The
-- naturals, the order relation on them, etc. are likewise all defined
-- constructively.

module 4SWC where

-- Just to take care of the universe levels; you can safely ignore it:
open import Agda.Primitive

------------------------------------------------
-------- DEFINITIONS: ℕ, Void, ≤, and Σ --------
------------------------------------------------

-- The naturals are (freely generated by) zero and successor. Though it's called
-- "Set", it isn't a ZFC set or anything like it. It's just part of the language
-- of Agda; saying `T : Set` means that T is a type.
data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

-- The empty type has no constructors:
data Void : Set where

-- In keeping with the propositions-are-types perspective, we define ≤ to be a
-- family of types; namely, the types of proofs that one natural is ≤ another.
data _≤_ : ℕ → ℕ → Set where
  -- Zero is ≤ everything:
  Z-min : {  n : ℕ} → Z ≤ n
  -- Succession is order-preserving:
  S-ord : {m n : ℕ} → m ≤ n → S m ≤ S n

-- Dependent pair (Cartesian product). That is, its elements are (x,y), where
-- the type of y can depend on x. This models existential quantification, which
-- we need to state the proofs. Again, you can ignore the universe levels (the
-- ℓ's).
data Σ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  _,_ : (a : A) → (b : B a) → Σ A B


--------------------------
-- DEFINITION: NEGATION --
--------------------------

-- When doing things type-theoretically like this, function types (or, by CHI,
-- implication) are more fundamental than `¬`, so we define the latter in terms
-- of the former. NAmely, we say that "a type Not(T) is inhabited" if and only
-- if "from an element of T, we can construct an element of the empty type".
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ T = (T → Void)

-- Note that this is *NOT* classical. In constructive math, proofs by negation
-- and proofs by contradiction are completely different, and only the former is
-- valid. The latter can't be constructed in Agda without an added `postulate`
-- for LEM, and once you do that, you lose all the nice computation properties
-- that the CHI gives you.

----------------------------
-- THE CONSTRUCTION/PROOF --
----------------------------

-- Here's the main lemma we need: ¬(S n ≤ n).
≤-not-suc-dec : {n : ℕ} → ¬(S n ≤ n)
≤-not-suc-dec (S-ord p) = ≤-not-suc-dec p

-- A constructed term inhabiting the type "there is no biggest natural".
no-biggest-nat : ¬(Σ ℕ (λ {n → ((m : ℕ) → (m ≤ n))}))
no-biggest-nat (n , f) = ≤-not-suc-dec (f (S n))