Ordinals

Content created by Fernando Chu.

Created on 2024-08-05.
Last modified on 2024-08-05.

module order-theory.ordinals 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-orders
open import order-theory.well-founded-relations

Idea

An ordinal is a propositional relation that is

  • Transitive: R x y and R y z imply R x y.
  • Extensional: R x y and R y x imply x ＝ y.
  • Well-founded: a structure on which it is well-defined to do induction.

In other words, it is a well-founded order that is Prop-valued and antisymmetric.

Definitions

The predicate of being an ordinal

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

  is-ordinal : UU (l1 ⊔ l2)
  is-ordinal =
    is-well-founded-order-Relation (type-Relation-Prop R) ×
    is-antisymmetric (type-Relation-Prop R)

Ordinals

Ordinal : {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
Ordinal l2 X = Σ (Relation-Prop l2 X) is-ordinal

module _
  {l1 l2 : Level} {X : UU l1} (S : Ordinal l2 X)
  where

  lt-prop-Ordinal : Relation-Prop l2 X
  lt-prop-Ordinal = pr1 S

  lt-Ordinal : Relation l2 X
  lt-Ordinal = type-Relation-Prop lt-prop-Ordinal

  is-ordinal-Ordinal :
    is-ordinal lt-prop-Ordinal
  is-ordinal-Ordinal = pr2 S

  is-well-founded-order-Ordinal :
    is-well-founded-order-Relation lt-Ordinal
  is-well-founded-order-Ordinal = pr1 is-ordinal-Ordinal

  is-antisymmetric-Ordinal :
    is-antisymmetric lt-Ordinal
  is-antisymmetric-Ordinal = pr2 is-ordinal-Ordinal

  is-transitive-Ordinal : is-transitive lt-Ordinal
  is-transitive-Ordinal =
    pr1 is-well-founded-order-Ordinal

  is-well-founded-relation-Ordinal :
    is-well-founded-Relation lt-Ordinal
  is-well-founded-relation-Ordinal =
    pr2 is-well-founded-order-Ordinal

  well-founded-relation-Ordinal : Well-Founded-Relation l2 X
  pr1 well-founded-relation-Ordinal =
    lt-Ordinal
  pr2 well-founded-relation-Ordinal =
    is-well-founded-relation-Ordinal

  is-asymmetric-Ordinal :
    is-asymmetric lt-Ordinal
  is-asymmetric-Ordinal =
    is-asymmetric-Well-Founded-Relation well-founded-relation-Ordinal

  is-irreflexive-Ordinal :
    is-irreflexive lt-Ordinal
  is-irreflexive-Ordinal =
    is-irreflexive-Well-Founded-Relation
      ( well-founded-relation-Ordinal)

Recent changes