eqInt

import nat (+)
import integer (Int)
import integerNormalize (normPair, normSound, intNormalize)
import equality (sym, trans)
import prop (↔, iffIntro)

-- Observational equality of Int, and its logical equivalence with the
-- built-in ≡ ∈ El Int. Int is a quotient (ℕ ⨯ ℕ) / IntR, so its OWN
-- defining relation is already the natural "observational" candidate —
-- but lifting IntR to El Int × El Int directly (via a double quot-elim
-- landing in Ω) needs its well-definedness proved as an Ω-code
-- equality, i.e. propositional extensionality between two DIFFERENT
-- IntR-applications, and this elaborator's propext check only
-- discharges the evident (𝟙-/reflexive-≡-shaped) cases automatically —
-- it does not search for the mutual-implication witnesses even when
-- they're sitting in context (see the prop.nova-only bonus attempt in
-- the sibling eqNat.nova). So EqI instead compares CANONICAL
-- representatives (integerNormalize.nova's intNormalize), squashing an
-- ordinary EQUATION rather than an Ω-code — equations are
-- proof-irrelevant (every ≡-proof is ⋆ on the nose), so THIS
-- well-definedness is free.

-- IntR is Int's own quotient relation, named for reuse; a proof of it
-- gives equal classes directly (el-quot-eq, automatic given a term of
-- Prf (IntR p q) in context — no extra machinery needed).
def IntR : (ℕ ⨯ ℕ) → (ℕ ⨯ ℕ) → Ω ≔ λp. λq. (p .π₁ + q .π₂ ≡ p .π₂ + q .π₁ ∈ ℕ)

def classEqOfRel : (p : ℕ ⨯ ℕ) (q : ℕ ⨯ ℕ) → Prf (IntR p q) → class p ≡ class q ∈ El Int ≔
  λp. λq. λh. ⋆

-- normPair's own representative is IntR-related to its input (that's
-- normSound), so its class is the same Int
def classNormPairEq : (p : ℕ ⨯ ℕ) → class (normPair (p .π₁) (p .π₂)) ≡ class p ∈ El Int ≔
  λp. classEqOfRel (normPair (p .π₁) (p .π₂)) p (normSound (p .π₁) (p .π₂))

-- normalization doesn't change the value: intNormalize z is z. The
-- quot-elim's well-definedness goal here is an EQUATION (not an Ω
-- code), so it's discharged for free by proof irrelevance regardless
-- of how the representative varies.
def intNormalizeId : (z : El Int) → intNormalize z ≡ z ∈ El Int ≔
  λz. quot-elim (w. intNormalize w ≡ w ∈ El Int) (p. classNormPairEq p) z

-- a squashed equality at any 𝕌-code reflects into a judgemental one —
-- prop.nova's reflectSquash generalized (that one is hardcoded to ℕ);
-- Int being a genuine 𝕌-code term (not a `type` item) is what makes
-- this reusable, generic combinator applicable to it at all
def reflectSquashAt : (A : 𝕌) (a : El A) (b : El A) (h : Prf (a ≡ b ∈ El A)) → a ≡ b ∈ El A ≔
  λA. λa. λb. λh. ⋆

def EqI : El Int → El Int → Ω ≔ λz1. λz2. (intNormalize z1 ≡ intNormalize z2 ∈ El Int)

def eqIRefl : (z : El Int) → Prf (EqI z z) ≔ λz. ⋆

-- soundness: z1 and z2 both equal their own normalizations, which
-- coincide whenever EqI holds
def eqISound : (z1 : El Int) (z2 : El Int) → Prf (EqI z1 z2) → z1 ≡ z2 ∈ El Int ≔
  λz1. λz2. λh.
    trans _ _ _ _
      (sym _ _ _ (intNormalizeId z1))
      (trans _ _ _ _
        (reflectSquashAt _ _ _ h)
        (intNormalizeId z2))

-- completeness: z1 ≡ z2 reflects, so intNormalize z1 and intNormalize
-- z2 are the same term — the evident-≡-shape squashee bare ⋆ handles
def eqIComplete : (z1 : El Int) (z2 : El Int) → (z1 ≡ z2 ∈ El Int) → Prf (EqI z1 z2) ≔
  λz1. λz2. λh. ⋆

-- the logical equivalence, packaged with prop.nova's ↔ against the
-- squashed built-in equality
def eqISoundP : (z1 : El Int) (z2 : El Int) → Prf (EqI z1 z2) → Prf (z1 ≡ z2 ∈ El Int) ≔
  λz1. λz2. λh. eqISound _ _ h

def eqICompleteP : (z1 : El Int) (z2 : El Int) → Prf (z1 ≡ z2 ∈ El Int) → Prf (EqI z1 z2) ≔
  -- ∥Prf p∥ ≜ p (code-squash-prf): h already proves the equation
  λz1. λz2. λh. eqIComplete _ _ h

def eqIIff : (z1 : El Int) (z2 : El Int) → Prf (EqI z1 z2 ↔ (z1 ≡ z2 ∈ El Int)) ≔
  λz1. λz2. iffIntro _ _ (eqISoundP _ _) (eqICompleteP _ _)