module IntegerAlgebra where

open import Preliminaries
open import Equivalences

record IntAlg (X : Set) : Set where
  constructor mk-IntAlg
  field
    S : X ≅ X
    Z : X

module _ {X : Set} (X-alg : IntAlg X) where
  private module X = IntAlg X-alg

  record DIntAlg (Y : X → Set) : Set where
    constructor mk-DIntAlg
    field
      S : {x : X} → Y x ≅ Y (X.S .fun x)
      Z : Y X.Z

  record Sec {Y : X → Set} (Y-alg : DIntAlg Y) : Set where
    private module Y = DIntAlg Y-alg
    field
      on-C : (x : X) → Y x
      on-S : (x : X) → on-C (X.S .fun x) ≡ Y.S .fun (on-C x)
      on-Z : on-C X.Z ≡ Y.Z

  nonDIntAlg : {Y : Set} (Y-alg : IntAlg Y) → DIntAlg (λ x → Y)
  nonDIntAlg Y-alg .DIntAlg.S = IntAlg.S Y-alg
  nonDIntAlg Y-alg .DIntAlg.Z = IntAlg.Z Y-alg

postulate
  ℤ : Set
  ℤ-alg : IntAlg ℤ
  ℤ-elim : {Y : ℤ → Set} (Y-alg : DIntAlg ℤ-alg Y) → Sec ℤ-alg Y-alg

module ℤ = IntAlg ℤ-alg

module _ {P : ℤ → Set} (P-alg : DIntAlg ℤ-alg P) where
  private module P = DIntAlg P-alg

  abstract
    ℤ-ind : (x : ℤ) → P x
    ℤ-ind = Sec.on-C (ℤ-elim P-alg)

    ℤ-ind-S : (x : ℤ) → ℤ-ind (ℤ.S .fun x) ≡ P.S .fun (ℤ-ind x)
    ℤ-ind-S = Sec.on-S (ℤ-elim P-alg)

    ℤ-ind-Z : ℤ-ind ℤ.Z ≡ P.Z
    ℤ-ind-Z = Sec.on-Z (ℤ-elim P-alg)

module _ {P : Set} (P-alg : IntAlg P) where
  module P = IntAlg P-alg

  abstract
    ℤ-elim-nondep : Sec ℤ-alg (nonDIntAlg ℤ-alg P-alg)
    ℤ-elim-nondep = ℤ-elim _

    ℤ-rec : (x : ℤ) → P
    ℤ-rec = ℤ-ind $ nonDIntAlg _ P-alg

    ℤ-rec-S : (x : ℤ) → ℤ-rec (ℤ.S .fun x) ≡ P.S .fun (ℤ-rec x)
    ℤ-rec-S = ℤ-ind-S _

    ℤ-rec-inv : (x : ℤ) → ℤ-rec (ℤ.S .inv x) ≡ P.S .inv (ℤ-rec x)
    ℤ-rec-inv x = symm (ap (P.S .inv ∘ ℤ-rec) (symm $ ℤ.S .fun-inv x) • ap (P.S .inv) (ℤ-rec-S _) • P.S .inv-fun _)

    ℤ-rec-Z : ℤ-rec ℤ.Z ≡ P.Z
    ℤ-rec-Z = ℤ-ind-Z _

    ℤ-rec-uniq : {f g : ℤ → P} → ((x : ℤ) → f (ℤ.S .fun x) ≡ P.S .fun (f x)) → f ℤ.Z ≡ P.Z →
                 ((x : ℤ) → g (ℤ.S .fun x) ≡ P.S .fun (g x)) → g ℤ.Z ≡ P.Z →
                 (x : ℤ) → f x ≡ g x
    ℤ-rec-uniq {f} {g} fS fZ gS gZ = ℤ-ind $ mk-DIntAlg {Y = λ x → f x ≡ g x}
      (λ {x} → inv-iso (eq-congr (fS x) (gS x)) ∘ₑ ap-iso P.S)
      (fZ • symm gZ)