module M where

open import Preliminaries
open import IntegerAlgebra
open import NatAlgebra
open import Doubling
open import Signs
open import Subtraction
open import RollingRule
open import Equivalences

ℤ⁰ M : Set
ℤ⁰ = Σ ℤ zero
M = Σ ℤ nonneg

M-S-iso : M ≅ Σ ℤ pos
M-S-iso = Σ-congr ℤ.S $ λ x → transport-iso nonneg (symm (ℤ.S .inv-fun x))

+-iso-M : ℤ⁰ + M ≅ M
+-iso-M = Σ-congr-snd (λ x → zero+pos-iso-nonneg) ∘ₑ +-distrib ∘ₑ +-congr id-iso M-S-iso

M-inl : ℤ⁰ → M
M-inl = +-iso-M .fun ∘ inl

ℤ⁰-zero : ℤ⁰
ℤ⁰-zero = (ℤ.Z , zeroIsZero)

M-alg : NatAlg M
M-alg .NatAlg.S = +-iso-M .fun ∘ inr
M-alg .NatAlg.Z = M-inl ℤ⁰-zero

_<'_ : M → ℤ → Set
m <' u = m .fst < u

module M = NatAlg M-alg

M-S-ap-iso : {x y : M} → x ≡ y ≅ M.S x ≡ M.S y
M-S-ap-iso = ap-iso +-iso-M ∘ₑ ap-inr-iso

M-inl-ap-iso : {x y : ℤ⁰} → x ≡ y ≅ M-inl x ≡ M-inl y
M-inl-ap-iso = ap-iso +-iso-M ∘ₑ ap-inl-iso

module ifun (A : M → Set) (AZ : (m : ℤ⁰) → A (M-inl m)) (AS : (m : M) → A m → A (M.S m)) where
  private
    pfun : ℤ → Set
    pfun u = (m : M) → m <' u → A m

    res : (u : ℤ) → pfun (ℤ.S .fun u) → pfun u
    res u f m h = f m $ lt-succ-of-lt h

    abstract
      ext : (u : ℤ) → pfun u → pfun (ℤ.S .fun u)
      ext u f = equiv-ind +-iso-M $ +-ind (λ m _ → AZ m) λ m h → AS m $ f m $ lt-of-succ-lt-succ h

      ext-zero : {u : ℤ} {f : pfun u} {m : ℤ⁰} {h : M-inl m <' ℤ.S .fun u} →
              ext u f (M-inl m) h ≡ AZ m
      ext-zero {m = m} {h = h} = congrFun (equiv-ind-fun _ _ (inl m)) _

      ext-succ : {u : ℤ} (f : pfun u) {m : M} {h : M.S m <' ℤ.S .fun u} →
              ext u f (M.S m) h ≡ AS m (f m (lt-of-succ-lt-succ h))
      ext-succ f = congrFun (equiv-ind-fun _ _ (inr _)) _

    ext-res-eq-res-ext : {u : ℤ} (f : pfun (ℤ.S .fun u)) (m : M) (h : m <' ℤ.S .fun u) →
                        ext u (res u f) m h ≡ res (ℤ.S .fun u) (ext (ℤ.S .fun u) f) m h
    ext-res-eq-res-ext {u} f = equiv-ind +-iso-M $ +-ind
      (λ x h → ext-zero • symm ext-zero)
      (λ x h → ext-succ _ • ap (AS _ ∘ f _) (lt-prop _ _) • symm (ext-succ _))

    -- This is the only place where we use funext.
    pfun-eq : {u : ℤ} {f g : pfun u} → ((m : M) (h : m <' u) → f m h ≡ g m h) →
                      f ≡ g
    pfun-eq p = funext λ m → funext λ h → p m h

    inductive-fun : ℤ → Set
    inductive-fun u = fix (res u ∘ ext u)

    zero-indfun : inductive-fun ℤ.Z
    zero-indfun .fst m h = exfalso $ lt-zero-nonneg-disj h (m .snd)
    zero-indfun .snd = pfun-eq $ λ m h → exfalso $ lt-zero-nonneg-disj h (m .snd)

    abstract
      ind-succ : {u : ℤ} → inductive-fun u ≅ inductive-fun (ℤ.S .fun u)
      ind-succ {u} = fix-congr (λ f → pfun-eq $ ext-res-eq-res-ext f) ∘ₑ rolling-rule (ext u) (res u)

      ind-succ-S : {u : ℤ} {fi : inductive-fun u} {m : M} {h : M.S m <' ℤ.S .fun u} →
                   ind-succ .fun fi .fst (M.S m) h ≡ AS m (fi .fst m $ lt-of-succ-lt-succ h)
      ind-succ-S {fi = fi} = congrFun (congrFun (rolling-rule-fun _ _ _) _) _ • ext-succ (fi .fst)

    indfun-Z : {u : ℤ} {m : ℤ⁰} (fi : inductive-fun u) {h : M-inl m <' u} →
               fi .fst (M-inl m) h ≡ AZ m
    indfun-Z {u} {m} fi {h} = transport (λ g → g (M-inl m) h ≡ AZ m) ext-zero (fi .snd)

    ifun-alg : DIntAlg ℤ-alg inductive-fun
    ifun-alg .DIntAlg.S = ind-succ
    ifun-alg .DIntAlg.Z = zero-indfun

    M-ind-aux : (u : ℤ) → inductive-fun u
    M-ind-aux = ℤ-ind ifun-alg

  abstract
    M-ind : (m : M) → A m
    M-ind m = M-ind-aux (M.S m .fst) .fst m lt-succ-self

    M-ind-zero : {m : ℤ⁰} → M-ind (M-inl m) ≡ AZ m
    M-ind-zero = indfun-Z (M-ind-aux _)

    M-ind-succ : (m : M) → M-ind (M.S m) ≡ AS m (M-ind m)
    M-ind-succ m = ap (λ fi → fi .fst (M.S m) lt-succ-self) (ℤ-ind-S ifun-alg (M.S m .fst)) •
                   ind-succ-S •
                   ap (AS m ∘ M-ind-aux (M.S m .fst) .fst m) (lt-prop _ _)