open import 1Lab.HLevel 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**:

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 : Wf β β {ββ²} (P : A β Type ββ²) β (β x β (β y β y < x β P y) β P x) β β x β P x Wf-induction wf P work x = go x (wf x) where go : β x β Acc x β P x go x (acc w) = work x (Ξ» y y<x β go y (w y y<x)) Induction-wf : (β {ββ²} (P : A β Type ββ²) β (β x β (β y β y < x β P y) β P x) β β x β P x) β Wf Induction-wf ind = ind Acc (Ξ» _ β acc)