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

-- The type of fixpoints of 'rectify'.
ℕ : 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