load "misc.quox"

namespace natw {

def0 Tag : ★ = {z, s}

def0 Child : Tag → ★ =
  λ t ⇒ case t return ★ of { 'z ⇒ {}; 's ⇒ {pred} }

def0 NatW : ★ = (t : Tag) ⊲ Child t

def Zero : NatW =
  'z ⋄ (λ v ⇒ case v return NatW of {})

def Suc : ω.NatW → NatW =
  λ n ⇒ 's ⋄ (λ u ⇒ case u return NatW of { 'pred ⇒ n })

def elim : 0.(P : NatW → ★) →
           ω.(P Zero) →
           ω.(0.(n : NatW) → ω.(P n) → P (Suc n)) →
           ω.(n : NatW) → P n =
  λ P pz ps n ⇒
  caseω n return n' ⇒ P n' of {
    t ⋄ f, ω.ih ⇒
      (case t
       return t' ⇒ 0.(eq : t ≡ t' : Tag) →
         P (t' ⋄ coe (𝑖 ⇒ ω.(Child (eq @𝑖)) → NatW) f)
       of {
         'z ⇒ λ _ ⇒ pz;
         's ⇒ λ eq ⇒
           ps (f  (coe (𝑖 ⇒ Child (eq @𝑖)) @1 @0 'pred))
              (ih (coe (𝑖 ⇒ Child (eq @𝑖)) @1 @0 'pred))
       }) (δ 𝑖 ⇒ t)
  }

}