36 lines
948 B
Text
36 lines
948 B
Text
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)
|
||
}
|
||
|
||
}
|