The based induction principle of the natural numbers

module elementary-number-theory.based-induction-natural-numbers where
Imports
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.functions
open import foundation.identity-types
open import foundation.universe-levels

Idea

The based induction principle for the natural numbers asserts that for any family P of types over and any natural number k : ℕ, equipped with

  1. An element p0 : P k
  2. A function pS : (x : ℕ) → k ≤-ℕ x → P x → P (x + 1) there is a function
  based-ind-ℕ k P p0 pS : (x : ℕ) → k ≤-ℕ x → P x

such that

  1. based-ind-ℕ k P p0 pS k K = p0 for any `K : k ≤-ℕ k, and
  2. based-ind-ℕ k P p0 pS (n + 1) N' = pS n N (based-ind-ℕ k P p0 pS n N for any N : k ≤-ℕ n and any N' : k ≤-ℕ n + 1.

Theorem

The based induction principle for the natural numbers

based-ind-ℕ :
  {l : Level} (k : ) (P :   UU l) 
  P k  ((n : )  k ≤-ℕ n  P n  P (succ-ℕ n))  (n : )  k ≤-ℕ n  P n
based-ind-ℕ zero-ℕ P p0 pS zero-ℕ H = p0
based-ind-ℕ zero-ℕ P p0 pS (succ-ℕ n) H =
  pS n H (based-ind-ℕ 0 P p0 pS n (leq-zero-ℕ n))
based-ind-ℕ (succ-ℕ k) P p0 pS (succ-ℕ n) =
  based-ind-ℕ k (P  succ-ℕ) p0 (pS  succ-ℕ) n

compute-base-based-ind-ℕ :
  {l : Level} (k : ) (P :   UU l) (p0 : P k) 
  (pS : (n : )  k ≤-ℕ n  P n  P (succ-ℕ n))  (H : k ≤-ℕ k) 
  based-ind-ℕ k P p0 pS k H  p0
compute-base-based-ind-ℕ zero-ℕ P p0 pS star = refl
compute-base-based-ind-ℕ (succ-ℕ k) P p0 pS =
  compute-base-based-ind-ℕ k (P  succ-ℕ) p0 (pS  succ-ℕ)

compute-succ-based-ind-ℕ :
  {l : Level} (k : ) (P :   UU l) (p0 : P k) 
  (pS : (n : )  k ≤-ℕ n  P n  P (succ-ℕ n)) 
  (n : ) (N : k ≤-ℕ n) (N' : k ≤-ℕ succ-ℕ n) 
  based-ind-ℕ k P p0 pS (succ-ℕ n) N' 
  pS n N (based-ind-ℕ k P p0 pS n N)
compute-succ-based-ind-ℕ zero-ℕ P p0 pS zero-ℕ star star = refl
compute-succ-based-ind-ℕ zero-ℕ P p0 pS (succ-ℕ n) star star = refl
compute-succ-based-ind-ℕ (succ-ℕ k) P p0 pS (succ-ℕ n) =
  compute-succ-based-ind-ℕ k (P  succ-ℕ) p0 (pS  succ-ℕ) n

See also