module Doubling where

open import Preliminaries
open import IntegerAlgebra

twist-alg : IntAlg (ℤ + ℤ)
twist-alg .IntAlg.S = +-symm ∘ₑ +-congr id-iso ℤ.S
twist-alg .IntAlg.Z = inl ℤ.Z

double-alg : {X : Set} → IntAlg X → IntAlg X
double-alg X-alg .IntAlg.S = X-alg .IntAlg.S ∘ₑ X-alg .IntAlg.S
double-alg X-alg .IntAlg.Z = X-alg .IntAlg.Z

abstract
  halve : ℤ → ℤ + ℤ
  halve = ℤ-rec twist-alg

  double : ℤ + ℤ → ℤ
  double = +-ind (ℤ-rec (double-alg ℤ-alg)) (ℤ.S .fun ∘ ℤ-rec (double-alg ℤ-alg))

  double-S : (x : ℤ + ℤ) → ℤ.S .fun (double x) ≡ double (twist-alg .IntAlg.S .fun x)
  double-S = +-ind (λ x → refl) λ x → symm (ℤ-rec-S (double-alg ℤ-alg) x)

  double-halve : (x : ℤ) → double (halve x) ≡ x
  double-halve = ℤ-rec-uniq ℤ-alg
    (λ x → ap double (ℤ-rec-S twist-alg x) • symm (double-S (halve x)))
    (ap double (ℤ-rec-Z _) • ℤ-rec-Z _)
    (λ _ → refl) refl

  halve-double : (x : ℤ) → halve (double (inl x)) ≡ inl x
  halve-double = ℤ-rec-uniq (double-alg twist-alg)
    (λ x → ap halve (ℤ-rec-S _ _) • ℤ-rec-S _ _ • ap (twist-alg .IntAlg.S .fun) (ℤ-rec-S twist-alg _))
    (ap halve (ℤ-rec-Z _) • ℤ-rec-Z _) (λ x → refl) refl

  halve-iso : ℤ ≅ ℤ + ℤ
  halve-iso .fun = halve
  halve-iso .inv = double
  halve-iso .inv-fun = double-halve
  halve-iso .fun-inv = +-ind halve-double λ x → ℤ-rec-S _ _ • ap (twist-alg .IntAlg.S .fun) (halve-double x)