integerAdd

import nat (+, plusZeroId, plusSucId, zeroPlusId, sucPlus, plusComm, plusAssoc, swapLeft)
import integer (Int)

-- ===== helpers for the well-definedness obligations =====

-- addition of pairs is well-defined in its second argument: the
-- cross-sum equation, conditional on the relation hypothesis
-- the relation is Ω-valued now, so the conditional hypothesis is the
-- squash Prf ∥…∥; reflection unsquashes it where the proof is used
def intAddWD : (a1 : ℕ) (a2 : ℕ) (b1 : ℕ) (b2 : ℕ) (c1 : ℕ) (c2 : ℕ) (h : Prf (b1 + c2 ≡ b2 + c1 ∈ ℕ)) →
  (a1 + b1) + (a2 + c2) ≡ (a2 + b2) + (a1 + c1) ∈ _ ≔
  λa1. λa2. λb1. λb2. λc1. λc2. λh. ℕ-elim (k. (a1 + b1) + (k + c2) ≡ (k + b2) + (a1 + c1) ∈ ℕ)
    ⋆ (k ih. ⋆) a2

-- cross-sum well-definedness in the OUTER argument, conditional on h
def intAddCross : (a1 : ℕ) (a2 : ℕ) (b1 : ℕ) (b2 : ℕ) (c1 : ℕ) (c2 : ℕ) (h : Prf (a1 + b2 ≡ a2 + b1 ∈ ℕ)) →
  (a1 + c1) + (b2 + c2) ≡ (a2 + c2) + (b1 + c1) ∈ ℕ ≔
  λa1. λa2. λb1. λb2. λc1. λc2. λh. ℕ-elim (k. (a1 + c1) + (b2 + k) ≡ (a2 + k) + (b1 + c1) ∈ ℕ)
    ⋆ (k ih. ⋆) c2

-- the same, one level up: the inner elimination is well-defined in the
-- OUTER argument — proven by quotient elimination with an ≡-motive
def intAddWDOuter : (a : ℕ ⨯ ℕ) (b : ℕ ⨯ ℕ) (h : Prf (a .π₁ + b .π₂ ≡ a .π₂ + b .π₁ ∈ ℕ)) (zy : El Int) →
  quot-elim (z. El Int) (x. class (a .π₁ + x .π₁ , a .π₂ + x .π₂)) zy
    ≡ quot-elim (z. El Int) (x. class (b .π₁ + x .π₁ , b .π₂ + x .π₂)) zy
    ∈ El Int ≔
  λa. λb. λh. λzy. quot-elim
    (q. quot-elim (z. El Int) (x. class (a .π₁ + x .π₁ , a .π₂ + x .π₂)) q
          ≡ quot-elim (z. El Int) (x. class (b .π₁ + x .π₁ , b .π₂ + x .π₂)) q
          ∈ El Int)
    (c. ⋆)
    zy

def intAdd : El Int → El Int → El Int ≔
  λzx. λzy.
    quot-elim (z. El Int)
      (a. quot-elim (z. El Int)
            (b. class (a .π₁ + b .π₁ , a .π₂ + b .π₂))
            zy)
      zx

def intAddTest : intAdd (class (Z , Z)) (class (S Z , S Z)) ≡ class (S Z , S Z) ∈ El Int ≔ ⋆

-- ===== the algebra =====

-- commutativity: two quotient eliminations at ≡-motives reduce to the
-- representative-level cross-sum permutation
def intAddComm : (x : El Int) (y : El Int) → intAdd x y ≡ intAdd y x ∈ _ ≔
  λx. λy. quot-elim
    (q. intAdd q y ≡ intAdd y q ∈ El Int)
    (a. quot-elim
          (q. intAdd (class a) q ≡ intAdd q (class a) ∈ El Int)
          (b. ⋆)
          y)
    x

-- associativity: three eliminations; the representatives reassociate
-- by plusAssoc and close by commutativity of the cross sum
def intAddAssoc : (x : El Int) (y : El Int) (z : El Int) →
  intAdd (intAdd x y) z ≡ intAdd x (intAdd y z) ∈ _ ≔
  λx. λy. λz. quot-elim
    (q. intAdd (intAdd q y) z ≡ intAdd q (intAdd y z) ∈ _)
    (a. quot-elim
          (q. intAdd (intAdd (class a) q) z ≡ intAdd (class a) (intAdd q z) ∈ _)
          (b. quot-elim
                (q. intAdd (intAdd (class a) (class b)) q
                      ≡ intAdd (class a) (intAdd (class b) q) ∈ _)
                (c. ⋆)
                z)
          y)
    x