module NatFeedback where

data Nat : Set where
  z : Nat
  s : Nat → Nat

_+_ : Nat → Nat → Nat
z   + n = n
s m + n = s (m + n)

data True : Set where
  tt : True

data False : Set where

_≡_ : Nat → Nat → Set 
z   ≡ z   = True
z   ≡ s _ = False
s _ ≡ z   = False
s m ≡ s n = m ≡ n

infix 10 _≡_

suc+ : (m n : Nat) → s m + n ≡ m + s n
suc+ z z     = tt
suc+ z (s y) = suc+ z y
suc+ (s y) z = suc+ y z
suc+ (s y) (s y') = suc+ y (s y')

ack : (x y : Nat) → Nat
ack z     n      = s n
ack (s y) z      = ack y (s z)
ack (s y) (s y') = ack y (ack (s y) y')

trans≡ : ∀ n n' n'' → n ≡ n' → n' ≡ n'' → n ≡ n''
trans≡ z z     n'' p q = q
trans≡ z (s y) n'' () q
trans≡ (s y) z n'' () q
trans≡ (s y) (s y') z p q = q
trans≡ (s y) (s y') (s y0) p q = trans≡ y y' y0 p q

data _≅_ : Nat → Nat → Set where
  zeq : z ≅ z
  seq : ∀{m n} → m ≅ n → s m ≅ s n

trans≅ : ∀{n n' n''} → n ≅ n' → n' ≅ n'' → n ≅ n''
trans≅ zeq     zeq     = zeq
trans≅ (seq p) (seq q) = seq (trans≅ p q)

data _≃_ : Nat → Nat → Set where
  refl : ∀{n} → n ≃ n

trans≃ : ∀{n n' n''} → n ≃ n' → n' ≃ n'' → n ≃ n''
trans≃ refl refl = refl