Natural.eq

-- Observational equality of natural numbers, defined in Ω, and its
-- logical equivalence with the built-in (parametric) equality type
-- ≡ ∈ ℕ. EqN is the classical double recursion: Z ~ Z and S n ~ S m
-- reduce further, any Z/S mismatch lands at ⊥.

import Core.prelude (constP)
import Core.prop (⊤, ⊥, ↔, iffIntro, reflectSquash, isZeroCode)
import Core.equality (cong, sym, transport)

EqN : ℕ → ℕ → Ω
EqN = λn. ℕ-elim (λm. ℕ-elim ⊤ (k ih. ⊥) m) (n ih. λm. ℕ-elim ⊥ (k ih2. ih k) m) n

eqNRefl : (n : ℕ) → EqN n n using (Natural.eq.EqN.eq, Natural.eq.EqN.unfold, Core.prop.⊤.unfold)
eqNRefl = λn. ℕ-elim ⋆ (k ih. ih) n

-- soundness: EqN implies the built-in equality — the Z/S-mismatch
-- cases are absurd (h squashes to 𝟘, which proves anything, including
-- an equation), the matching cases fall out of the inductive
-- hypothesis by congruence on S
eqNSound : {n m : ℕ} → EqN n m → n ≡ m
  using (Natural.eq.EqN.eq, Natural.eq.EqN.unfold, Core.prop.propext, Core.prop.⊥.unfold)
eqNSound =
  λn. ℕ-elim
    λm. ℕ-elim (constP ⋆) (j ih2. λh. reflectSquash (squash-elim h (x. 𝟘-elim x))) m
    n ih. λm. ℕ-elim (λh. reflectSquash (squash-elim h (x. 𝟘-elim x))) (j ih2. λh. ih j h) m
    n

-- ℕ has no confusion between Z and S _: transporting Core/prop.nova's
-- "is-Z" code along a bad Z ≡ S j equation lands a 𝟙-witness in 𝟘
-- (Core.prop.absurd is the j = Z instance, composed with absurdP)
zNotS : {j : ℕ} → (Z ≡ S j) → 𝟘 using (Core.prop.isZeroCode.unfold)
zNotS = λj h. transport isZeroCode h ()

-- S is injective: predecessor congruence recovers n ≡ j from S n ≡ S j
pred : ℕ → ℕ
pred = λn. ℕ-elim Z (n ih. n) n

predEq : {n j : ℕ} → (S n ≡ S j) → n ≡ j
predEq = λn j h. cong (λ_. ℕ) pred h

-- completeness: the built-in equality implies EqN, by double
-- induction mirroring EqN's own recursion — the Z/S-mismatch cases
-- are impossible (absurd via zNotS), the matching cases recurse
eqNComplete : {n m : ℕ} → (n ≡ m) → EqN n m
  using (Natural.eq.EqN.eq, Natural.eq.EqN.unfold, Core.prop.⊤.unfold)
eqNComplete =
  λn. ℕ-elim
    λm. ℕ-elim (λh. ⋆) (j ih2. λh. 𝟘-elim (zNotS h)) m
    n ih. λm. ℕ-elim (λh. 𝟘-elim (zNotS (sym _ _ h))) (j ih2. λh. ih j (predEq {j} {n} h)) m
    n

-- the logical equivalence, packaged with Core/prop.nova's ↔ against the
-- squashed built-in equality (Ω is impredicative, ≡ ∈ ℕ is not, so
-- ∥-∥ is the bridge)
eqNSoundP : {n m : ℕ} → EqN n m → n ≡ m
eqNSoundP = λn m h. ⋆ (eqNSound h)

-- ∥p∥ ≜ p (code-squash-prf): h already proves the equation
eqNCompleteP : {n m : ℕ} → (n ≡ m) → EqN n m using (Natural.eq.EqN.unfold)
eqNCompleteP = λn m h. eqNComplete h

eqNIff : (n m : ℕ) → EqN n m ↔ (n ≡ m) using (Core.prop.↔.unfold, Core.prop.∧.unfold)
eqNIff = λn m. iffIntro eqNSoundP eqNCompleteP