module Data.Wellfounded.Properties where
It was mentioned in the definition of Acc that that being accessible is a proposition, but this has not yet been established. We can do so using, as usual, induction:
Acc-is-prop : β x β is-prop (Acc R x) Acc-is-prop x (acc s) (acc t) = ap acc (funext Ξ» y β funext Ξ» y<x β Acc-is-prop y (s y y<x) (t y y<x)) Wf-is-prop : is-prop (Wf R) Wf-is-prop = Ξ -is-hlevel 1 Acc-is-prop
Instancesπ
The usual induction principle for the natural numbers is equivalent to saying that the relation is well-founded. Additionally, the relation on the natural numbers is well-founded.
suc-wf : Wf (Ξ» x y β y β‘ suc x) suc-wf = Induction-wf (Ξ» x y β y β‘ suc x) Ξ» P m β Nat-elim P (m 0 Ξ» y 0=suc β absurd (zeroβ suc 0=suc)) Ξ» {n} Pn β m (suc n) (Ξ» y s β subst P (suc-inj s) Pn) <-wf : Wf _<_ <-wf x = go x x β€-refl where go : (x y : Nat) β .(y β€ x) β Acc _<_ y go x zero w = acc Ξ» _ () go (suc x) (suc y) w = acc kβ² where kβ² : β x β x < suc y β Acc _<_ x kβ² xβ² wβ² = go x xβ² (β€-trans (β€-peel wβ²) (β€-peel w))