Tom de Jong (adapted from Martin's MGS lecture notes)
18 September 2020
We show that the type of natural numbers enjoys the universal property of a
natural numbers object. We generalize
https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html#ℕ-is-nno
here from nondependent functions to dependent functions.
\begin{code}
{-# OPTIONS --safe --without-K #-}
module Naturals.UniversalProperty where
open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.FunExt
open import UF.Retracts
open import UF.Subsingletons
ℕ-induction-retract : funext 𝓤₀ 𝓤
→ (Y : ℕ → 𝓤 ̇ ) (y₀ : Y 0) (g : (n : ℕ) → Y n → Y (succ n))
→ (Σ h ꞉ (Π Y) , (h 0 ＝ y₀) ×
((n : ℕ) → h (succ n) ＝ g n (h n)))
◁ (Σ h ꞉ (Π Y) , h ＝ ℕ-induction y₀ g)
ℕ-induction-retract fe Y y₀ g = Σ-retract _ _ γ
where
γ : (h : Π Y)
→ (h 0 ＝ y₀) × ((n : ℕ) → h (succ n) ＝ g n (h n))
◁ (h ＝ ℕ-induction y₀ g)
γ h = (h 0 ＝ y₀) × ((n : ℕ) → h (succ n) ＝ g n (h n)) ◁⟨ i ⟩
(h ∼ ℕ-induction y₀ g) ◁⟨ ii ⟩
(h ＝ ℕ-induction y₀ g) ◀
where
ii = ≃-gives-◁ (≃-sym (≃-funext fe h (ℕ-induction y₀ g)))
i = r , s , η
where
r : h ∼ ℕ-induction y₀ g
→ (h 0 ＝ y₀) × ((n : ℕ) → h (succ n) ＝ g n (h n))
r H = H 0 , (λ n → h (succ n) ＝⟨ H (succ n) ⟩
ℕ-induction y₀ g (succ n) ＝⟨ refl ⟩
g n (ℕ-induction y₀ g n) ＝⟨ ap (g n) ((H n) ⁻¹) ⟩
g n (h n) ∎)
s : (h 0 ＝ y₀) × ((n : ℕ) → h (succ n) ＝ g n (h n))
→ h ∼ ℕ-induction y₀ g
s (p , K) 0 = p
s (p , K) (succ n) = h (succ n) ＝⟨ K n ⟩
g n (h n) ＝⟨ ap (g n) (s (p , K) n) ⟩
g n (ℕ-induction y₀ g n) ＝⟨ refl ⟩
ℕ-induction y₀ g (succ n) ∎
η : r ∘ s ∼ id
η (p , K) =
r (s (p , K)) ＝⟨ refl ⟩
(p , λ n → s (p , K) (succ n)
∙ (refl ∙ ap (g n) ((s (p , K) n) ⁻¹))) ＝⟨ φ ⟩
(p , K) ∎
where
φ = ap (p ,_) (dfunext fe ψ)
where
ψ : (n : ℕ)
→ s (p , K) (succ n) ∙ (refl ∙ ap (g n) (s (p , K) n ⁻¹))
＝ K n
ψ n = s (p , K) (succ n)
∙ (refl ∙ ap (g n) (s (p , K) n ⁻¹)) ＝⟨ refl ⟩
K n ∙ ap (g n) (s (p , K) n)
∙ (refl ∙ ap (g n) ((s (p , K) n) ⁻¹)) ＝⟨ I ⟩
K n ∙ ap (g n) (s (p , K) n)
∙ ap (g n) ((s (p , K) n) ⁻¹) ＝⟨ II ⟩
K n ∙ (ap (g n) (s (p , K) n)
∙ ap (g n) ((s (p , K) n) ⁻¹)) ＝⟨ III ⟩
K n ∙ (ap (g n) (s (p , K) n)
∙ (ap (g n) (s (p , K) n)) ⁻¹) ＝⟨ IV ⟩
K n ∙ refl ＝⟨ refl ⟩
K n ∎
where
I = ap (K n ∙ ap (g n) (s (p , K) n) ∙_)
(refl-left-neutral {_} {_} {_} {_}
{ap (g n) ((s (p , K) n) ⁻¹)})
II = ∙assoc
(K n)
(ap (g n) (s (p , K) n))
(ap (g n) ((s (p , K) n) ⁻¹))
III = ap (λ - → K n ∙ (ap (g n) (s (p , K) n) ∙ -))
((ap-sym (g n) (s (p , K) n)) ⁻¹)
IV = ap (K n ∙_)
((right-inverse (ap (g n) (s (p , K) n))) ⁻¹)
ℕ-is-nno-dep : funext 𝓤₀ 𝓤
→ (Y : ℕ → 𝓤 ̇ ) (y₀ : Y 0) (g : (n : ℕ) → Y n → Y (succ n))
→ ∃! h ꞉ (Π Y) , ((h 0 ＝ y₀) × ((n : ℕ) → h (succ n) ＝ g n (h n)))
ℕ-is-nno-dep {𝓤} fe Y y₀ g = γ
where
γ : is-singleton
(Σ h ꞉ (Π Y) , (h 0 ＝ y₀) × ((n : ℕ) → h (succ n) ＝ g n (h n)))
γ = retract-of-singleton (ℕ-induction-retract fe Y y₀ g)
(singleton-types'-are-singletons (ℕ-induction {𝓤} {Y} y₀ g))
\end{code}