# Well-founded orders

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

Created 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)