Well-founded orders

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-orders where
Imports 
open import foundation.binary-relations
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import order-theory.well-founded-relations

Idea

A well-founded order is a transitive well-founded relation.

Definitions

The predicate of being a well-founded order

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

  is-well-founded-order-Relation : UU (l1 ⊔ l2)
  is-well-founded-order-Relation = is-transitive R × is-well-founded-Relation R

Well-founded orders

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

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

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

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

  is-transitive-Well-Founded-Order : is-transitive rel-Well-Founded-Order
  is-transitive-Well-Founded-Order =
    pr1 is-well-founded-order-Well-Founded-Order

  is-well-founded-relation-Well-Founded-Order :
    is-well-founded-Relation rel-Well-Founded-Order
  is-well-founded-relation-Well-Founded-Order =
    pr2 is-well-founded-order-Well-Founded-Order

  well-founded-relation-Well-Founded-Order : Well-Founded-Relation l2 X
  pr1 well-founded-relation-Well-Founded-Order =
    rel-Well-Founded-Order
  pr2 well-founded-relation-Well-Founded-Order =
    is-well-founded-relation-Well-Founded-Order

  is-asymmetric-Well-Founded-Order :
    is-asymmetric rel-Well-Founded-Order
  is-asymmetric-Well-Founded-Order =
    is-asymmetric-Well-Founded-Relation well-founded-relation-Well-Founded-Order

  is-irreflexive-Well-Founded-Order :
    is-irreflexive rel-Well-Founded-Order
  is-irreflexive-Well-Founded-Order =
    is-irreflexive-Well-Founded-Relation
      ( well-founded-relation-Well-Founded-Order)

Recent changes