open import 1Lab.Path
open import 1Lab.Type

module Data.Wellfounded.Base where


# Well-founded relationsπ

Well-founded relations are, in essence, orders over which induction is acceptable. A relation is well-founded if all of its chains have bounded length, which we can summarize with the following inductive definition of accessibility:

module _ {β β'} {A : Type β} (_<_ : A β A β Type β') where

  data Acc (x : A) : Type (β β β') where
acc : (β y β y < x β Acc y) β Acc x


That is, an element $x : A$ is accessible if every element $y < x$ under it (by the relation $<$) is also accessible. Paraphrasing the HoTT book, it may seem like such a definition can never get started, but the βbase caseβ is when there are no elements $y < x$ β for example, taking $<$ to be the usual $<$ on the natural numbers, there are no numbers $y < 0$, so $0$ is accessible.

A relation is well-founded if every $x : A$ is accessible.

  Wf : Type _
Wf = β x β Acc x


Being well-founded implies that we support induction, and conversely, any relation supporting induction is well-founded, by taking the motive $P$ to be the proposition β$x$ is accessibleβ.

  Wf-induction'
: β {β'} (P : A β Type β')
β (β x β (β y β y < x β P y) β P x)
β β x β Acc x β P x
Wf-induction' P work = go where
go : β x β Acc x β P x
go x (acc w) = work x (Ξ» y y<x β go y (w y y<x))

Wf-induction
: Wf β β {β'} (P : A β Type β')
β (β x β (β y β y < x β P y) β P x)
β β x β P x
Wf-induction wf P work x = Wf-induction' P work x (wf x)

Induction-wf
: (β {β'} (P : A β Type β') β (β x β (β y β y < x β P y) β P x) β β x β P x)
β Wf
Induction-wf ind = ind Acc (Ξ» _ β acc)