Purely axiomatic proof of +-comm on nat in extensional type theory

N-add-comm-lf.agda

variable
  A B : Set
postulate
  Eq : A → A → Set
  refl : (a : A) → Eq a a
  rw : {x y : A} → Eq x y → (B : A → Set) → B x → B y
  -- UIP missing but not needed
  N : Set
  Z : N
  S : N → N
  N-rec : (P : N → Set) → P Z → ((n : N) → P n → P (S n)) → (x : N) → P x
  N-β-1 : (P : N → Set) → {a : P Z} → {b : (n : N) → P n → P (S n)} → Eq (N-rec P a b Z) a
  N-β-2 : (P : N → Set) → {a : P Z} → {b : (n : N) → P n → P (S n)} → (m : N) → Eq (N-rec P a b (S m)) (b m (N-rec P a b m))

sym : {x y : A} → Eq x y → Eq y x
sym = λ z → rw z (λ z → Eq z _) (refl _)

trans : {x y z : A} → Eq x y → Eq y z → Eq x z
trans = λ z w → rw w (Eq _) z

cong : (f : A → B) → {x y : A} → Eq x y → Eq (f x) (f y)
cong f = λ z → rw z (λ w → Eq (f _) (f w)) (refl (f _))

module Version2 where
 postulate
  N-add : N → N → N
  N-add-0 : (a : N) → Eq (N-add a Z) a
  N-add-S : (a b : N) → Eq (N-add a (S b)) (S (N-add a b))
  N-add-0' : (a : N) → Eq (N-add Z a) a
  N-add-S' : (a b : N) → Eq (N-add (S a) b) (S (N-add a b))

 N-add-comm : (a b : N) → Eq (N-add a b) (N-add b a)
 N-add-comm a b = N-rec (λ x → Eq (N-add x b) (N-add b x))
  (trans (N-add-0' b) (sym (N-add-0 b)))
  (λ n x → trans (N-add-S' n b) (trans (cong S x) (sym (N-add-S b n)))) a

 N-add-assoc : (a b c : N) → Eq (N-add a (N-add b c)) (N-add (N-add a b) c)
 N-add-assoc a b c = N-rec (λ x → Eq (N-add x (N-add b c)) (N-add (N-add x b) c))
  (trans (N-add-0' (N-add b c)) (sym (cong add-c (N-add-0' b))))
  (λ n x → trans (N-add-S' n (N-add b c))
  (trans (trans (cong S x) (sym (N-add-S' (N-add n b) c)))
  (cong add-c (sym (N-add-S' n b))))) a
  where add-c = λ x → N-add x c

module Version1 where
 N-add : N → N → N
 N-add a b = N-rec (λ _ → N) a (λ _ → S) b

 N-add-comm : (a b : N) → Eq (N-add a b) (N-add b a)
 N-add-comm a b = N-rec (λ a' → Eq (N-add a' b) (N-add b a'))
  (trans (id1 b) (sym (jeq2 b)))
  (λ n p → trans (id2 n b) (trans (cong S p) (sym (jeq1 b n)))) a
  where
  P = λ (_ : N) → N
  jeq1 : ∀ a b → Eq (N-add a (S b)) (S (N-add a b))
  jeq1 a b = N-β-2 P b
  jeq2 : ∀ b → Eq (N-add b Z) b
  jeq2 b = N-β-1 P

  id1-lem : ∀ n → Eq (N-add Z n) n → Eq (N-add Z (S n)) (S n)
  id1-lem n p = rw (sym (jeq1 Z n)) (λ x → Eq x (S n)) (cong S p)
  id1 : ∀ b → Eq (N-add Z b) b
  id1 b = N-rec (λ b' → Eq (N-add Z b') b') (jeq2 Z) id1-lem b

  jeq3 : ∀ a → Eq (N-add (S a) Z) (S (N-add a Z))
  jeq3 a = trans (jeq2 (S a)) (cong S (sym (jeq2 a)))

  id2 : ∀ a b → Eq (N-add (S a) b) (S (N-add a b))
  id2 a b = N-rec (λ b' → Eq (N-add (S a) b') (S (N-add a b')))
    (jeq3 a) (λ n q → trans (jeq1 (S a) n) (cong S (trans q (sym (jeq1 a n))))) b

  chase-2023-11-19 : (a : N) → Eq (N-add (S a) Z) (S (N-add a Z))
  chase-2023-11-19 = λ a → rw (sym (N-β-1 P))
    (λ x → Eq (N-rec P (S a) (λ _ → S) Z) (S x)) (N-β-1 P)