{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

data ℕ : Type where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + m = m
suc n + m = suc (n + m)

data ℤ : Type where
  pos  : ℕ → ℤ
  -suc : ℕ → ℤ

_-_ : ℕ → ℕ → ℤ
n - zero = pos n
zero - suc m = -suc m
suc n - suc m = n - m

data ℤ' : Type where
  ⟨_,_⟩ : ℕ → ℕ → ℤ'
  cancel : ∀ (a b : ℕ) → ⟨ a , b ⟩ ≡ ⟨ suc a , suc b ⟩

toℤ : ℤ' → ℤ
toℤ ⟨ a , b ⟩ = b - a
toℤ (cancel a b i) = b - a

toℤ' : ℤ → ℤ'
toℤ' (pos x) = ⟨ zero , x ⟩
toℤ' (-suc x) = ⟨ (suc x) , zero ⟩

cancel-suc : ∀ (a b : ℕ) i → cancel a b i ≡ cancel (suc a) (suc b) i
cancel-suc a b i j = hcomp
  (λ k → λ {
    (i = i0) → cancel a b j;
    (i = i1) → cancel (suc a) (suc b) (j ∧ k);
    (j = i0) → cancel a b i;
    (j = i1) → cancel (suc a) (suc b) (i ∧ k)})
  (cancel a b (i ∨ j))

cancelm : ∀ (a b : ℕ) i → ⟨ a , b ⟩ ≡ cancel a b i
cancelm a b i j = hcomp
  (λ k → λ { (i = i0) → ⟨ a , b ⟩;
             (j = i0) → ⟨ a , b ⟩;
             (j = i1) → cancel a b (i ∧ k)})
  ⟨ a , b ⟩

right : section toℤ' toℤ
right ⟨ zero , b ⟩ = refl
right ⟨ suc a , zero ⟩ = refl
right ⟨ suc a , suc b ⟩ = right ⟨ a , b ⟩ ∙ (cancel a b)
right (cancel zero b i) = cancelm zero b i
right (cancel (suc a) zero i) = cancelm (suc a) zero i
right (cancel (suc a) (suc b) i) = (right (cancel a b i)) ∙ cancel-suc a b i

left : retract toℤ' toℤ
left (pos x) = refl
left (-suc x) = refl

isoℤ : Iso ℤ ℤ'
isoℤ .Iso.fun = toℤ'
isoℤ .Iso.inv = toℤ
isoℤ .Iso.rightInv = right
isoℤ .Iso.leftInv = left

ℤ≡ℤ' : ℤ ≡ ℤ'
ℤ≡ℤ' = isoToPath isoℤ