Well-founded relations

Content created by Daniel Gratzer, Egbert Rijke and Elisabeth Stenholm.

Created on 2023-11-27.
Last modified on 2023-11-27.

module order-theory.well-founded-relations where
open import foundation.action-on-identifications-functions
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.accessible-elements-relations


Given a type X equipped with a binary relation _ϵ_ : X → X → Type we say that the relation _ϵ_ is well-founded if all elements of X are accessible with respect to _ϵ_.

Well-founded relations satisfy an induction principle: In order to construct an element of P x for all x : X it suffices to construct an element of P y for all elements y ϵ x. More precisely, the well-founded induction principle is a function

  (x : X) → ((y : Y) → y ϵ x → P y) → P x.


The predicate of being a well-founded relation

module _
  {l1 l2 : Level} {X : UU l1} (_ϵ_ : Relation l2 X)

  is-well-founded-prop-Relation : Prop (l1  l2)
  is-well-founded-prop-Relation =
    Π-Prop X (is-accessible-element-prop-Relation _ϵ_)

  is-well-founded-Relation : UU (l1  l2)
  is-well-founded-Relation = (x : X)  is-accessible-element-Relation _ϵ_ x

Well-founded relations

Well-Founded-Relation : {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
Well-Founded-Relation l X = Σ (Relation l X) is-well-founded-Relation

module _
  {l1 l2 : Level} {X : UU l1} (R : Well-Founded-Relation l2 X)

  rel-Well-Founded-Relation : Relation l2 X
  rel-Well-Founded-Relation = pr1 R

  is-well-founded-Well-Founded-Relation :
    is-well-founded-Relation rel-Well-Founded-Relation
  is-well-founded-Well-Founded-Relation = pr2 R


Well-founded induction

module _
  {l1 l2 l3 : Level} {X : UU l1} ((_ϵ_ , w) : Well-Founded-Relation l2 X)
  (P : X  UU l3)

  ind-Well-Founded-Relation :
    ({x : X}  ({y : X}  y ϵ x  P y)  P x)  (x : X)  P x
  ind-Well-Founded-Relation IH x =
    ind-accessible-element-Relation _ϵ_ P  _  IH) (w x)

A well-founded relation is asymmetric (and thus irreflexive)

module _
  {l1 l2 : Level} {X : UU l1} ((_ϵ_ , w) : Well-Founded-Relation l2 X)

  is-asymmetric-Well-Founded-Relation :
    is-asymmetric _ϵ_
  is-asymmetric-Well-Founded-Relation x y =
    is-asymmetric-is-accessible-element-Relation _ϵ_ (w x)

module _
  {l1 l2 : Level} {X : UU l1} (ϵ : Well-Founded-Relation l2 X)

  is-irreflexive-Well-Founded-Relation :
    is-irreflexive (rel-Well-Founded-Relation ϵ)
  is-irreflexive-Well-Founded-Relation =
      ( rel-Well-Founded-Relation ϵ)
      ( is-asymmetric-Well-Founded-Relation ϵ)

Recent changes