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:Ax : A is accessible if every element y<xy < 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<xy < x β€” for example, taking << to be the usual << on the natural numbers, there are no numbers y<0y < 0, so 00 is accessible.

A relation is well-founded if every x:Ax : 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 PP to be the proposition β€œxx 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)