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