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}