module Naturals where
open import Preliminaries
open import Equivalences
open import NatAlgebra
open import M
open import RollingRule
private module Rect = ifun (λ _ → M) (λ _ → M.Z) (λ _ → M.S)
rectify : M → M
rectify = Rect.M-ind
rectify-Z : {m : ℤ⁰} → rectify (M-inl m) ≡ M.Z
rectify-Z = Rect.M-ind-zero
rectify-succ : {m : M} → rectify (M.S m) ≡ M.S (rectify m)
rectify-succ = Rect.M-ind-succ _
N : M → Set
N m = rectify m ≡ m
ℕ : Set
ℕ = Σ M N
N-zero : {m : ℤ⁰} → (ℤ⁰-zero ≡ m) ≅ N (M-inl m)
N-zero = eq-congr (symm rectify-Z) refl ∘ₑ M-inl-ap-iso
N-succ : (m : M) → N m ≅ N (M.S m)
N-succ m = eq-congr (symm rectify-succ) refl ∘ₑ M-S-ap-iso
N-alg : DNatAlg M-alg N
N-alg .DNatAlg.S = N-succ _ .fun
N-alg .DNatAlg.Z = N-zero .fun refl
ℕ-alg : NatAlg ℕ
ℕ-alg = Σ-alg M-alg N-alg
module ℕ = NatAlg ℕ-alg
module N = DNatAlg N-alg
module _ {P : ℕ → Set} (P-alg : DNatAlg ℕ-alg P) where
private
module PA = DNatAlg P-alg
A-fam : M → Set
A-fam m = ∀ (n : N m) → P (m , n)
A0-aux : {m : ℤ⁰} → (n : ℤ⁰-zero ≡ m) → P (M-inl m , N-zero .fun n)
A0-aux refl = PA.Z
A0 : (m : ℤ⁰) → A-fam (M-inl m)
A0 m = equiv-ind N-zero A0-aux
AS : (m : M) → A-fam m → A-fam (M.S m)
AS m a = equiv-ind (N-succ m) $ λ n → PA.S (a n)
AS-fun : (m : M) (a : A-fam m) (n : N m) → AS m a (N-succ m .fun n) ≡ PA.S (a n)
AS-fun m a = equiv-ind-fun (N-succ m) $ λ n → PA.S (a n)
module I = ifun A-fam A0 AS
P-sec : (n : ℕ) → P n
P-sec n = I.M-ind (n .fst) (n .snd)
P-sec-succ : (n : ℕ) → P-sec (ℕ.S n) ≡ PA.S (P-sec n)
P-sec-succ (m , n) = congrFun (I.M-ind-succ m) (N.S n) • AS-fun m (λ n' → P-sec (m , n')) n
P-sec-zero : P-sec ℕ.Z ≡ PA.Z
P-sec-zero = congrFun I.M-ind-zero N.Z • equiv-ind-fun _ _ _
ℕ-ind : NSec ℕ-alg P-alg
ℕ-ind .NSec.on-C = P-sec
ℕ-ind .NSec.on-S = P-sec-succ
ℕ-ind .NSec.on-Z = P-sec-zero