integerNormalize

import nat (+, plusZeroId, plusSucId, zeroPlusId)
import integer (Int)

-- the canonical representative: strip successors pairwise
def normPair : ℕ → ℕ → ℕ ⨯ ℕ ≔
  λa. ℕ-elim (k. ℕ → ℕ ⨯ ℕ)
        (λb. (Z , b))
        (n ih. λb. ℕ-elim (k. ℕ ⨯ ℕ) (S n , Z) (m ihb. ih m) b)
        a

-- normPair a b is R-related to (a, b)
def normSound : (a : ℕ) → (b : ℕ) →
  (normPair a b) .π₁ + b ≡ (normPair a b) .π₂ + a ∈ ℕ ≔
  λa.
    ℕ-elim (k. (b : ℕ) → (normPair k b) .π₁ + b ≡ (normPair k b) .π₂ + k ∈ ℕ)
      (λb. ⋆)
      (n ih. λb.
        ℕ-elim (m. (normPair (S n) m) .π₁ + m ≡ (normPair (S n) m) .π₂ + S n ∈ ℕ)
          ⋆
          (m ihb. ⋆)
          b)
      a

-- at the quotient, normalization is invisible
def normClass : (a : ℕ) (b : ℕ) → class (normPair a b) ≡ class (a , b) ∈ El Int ≔ λa. λb. ⋆

def intNormalize : El Int → El Int ≔
  λz. quot-elim (w. El Int) (rep. class (normPair (rep .π₁) (rep .π₂))) z

def intNormalizeTest1 : intNormalize (class (S Z , Z)) ≡ class (S Z , Z) ∈ El Int ≔ ⋆
def intNormalizeTest2 : intNormalize (class (S Z , S (S Z))) ≡ class (Z , S Z) ∈ El Int ≔ ⋆