open import 1Lab.Reflection.Record
open import 1Lab.Prelude

open import Data.Wellfounded.Properties hiding (<-wf)
open import Data.Wellfounded.Base

open import Order.Instances.Nat
open import Order.Univalent using (Poset-path)
open import Order.Subposet
open import Order.Base using (Poset)

import 1Lab.Reflection as Reflection

import Data.Nat.Order as Nat
import Data.Nat.Base as Nat
module Order.Ordinal.Base where

OrdinalsπŸ”—

An ordinal captures the concept of a well-founded order. Such an order is necessarily a strict order (like _<_, not _≀_), since a well-founded relation cannot be reflexive.

The conditions for a well-order an be expressed fairly concisely. A relation _<_ : X β†’ X β†’ Type is a well order if all of the following hold:

  • It is propositional.

  • It is well-founded.

  • It is transitive.

  • Whenever {z | z < x} ≑ {z | z < y}, we have x ≑ y.

Every ordinal is in fact a poset, where x ≀ y iff βˆ€ {z} β†’ z < x β†’ z < y. We choose to use a somewhat redundant definition of ordinal, where this poset is part of the structure, since it often lines up with a preexisting order.

record Ordinal (β„“ : Level) : Type (lsuc β„“) where
  no-eta-equality
  field
    poset : Poset β„“ β„“
  open Poset poset public
  field
    _<_ : Ob β†’ Ob β†’ Type β„“
    <-thin : βˆ€ {x y} β†’ is-prop (x < y)
    <-wf : Wf _<_
    <→≀ : βˆ€ {x y} β†’ x < y β†’ x ≀ y
    <→≀→< : βˆ€ {x y z} β†’ x < y β†’ y ≀ z β†’ x < z
    [<β†’<]→≀ : βˆ€ {x y} β†’ (βˆ€ {z} β†’ z < x β†’ z < y) β†’ (x ≀ y)
  <-trans : βˆ€ {x y z} β†’ x < y β†’ y < z β†’ x < z
  <-trans x<y y<z = <→≀→< x<y (<→≀ y<z)
  <-irrefl : βˆ€ {x} β†’ Β¬ (x < x)
  <-irrefl {x} x<x = go (<-wf x) where
    go : Β¬ Acc _<_ x
    go (acc h) = go (h x x<x)

  <-asym : βˆ€ {x y} β†’ x < y β†’ y < x β†’ βŠ₯
  <-asym x<y y<x = <-irrefl (<-trans x<y y<x)

private variable
  β„“ ℓ₁ β„“β‚‚ ℓ₃ : Level


module _ where
  instance
    Underlying-Ordinal : Underlying (Ordinal β„“)
    Underlying-Ordinal = record { ⌞_⌟ = Ordinal.Ob }

    open Reflection
    open hlevel-projection
    open hlevel-projection
    Ordinal-<-hlevel-proj : hlevel-projection (quote Ordinal._<_)
    Ordinal-<-hlevel-proj .has-level   = quote Ordinal.<-thin
    Ordinal-<-hlevel-proj .get-level _ = pure (lit (nat 1))
    Ordinal-<-hlevel-proj .get-argument (_ ∷ arg _ t ∷ _) = pure t
    Ordinal-<-hlevel-proj .get-argument _                     = typeError []

For example, the ordinal Ο‰ is given by the natural numbers, under their standard ordering.

Ο‰ : Ordinal lzero
Ο‰ = record where
  poset = Nat-poset
  _<_ = Nat._<_
  <-thin = Nat.≀-is-prop
  <→≀ = Nat.<-weaken
  <→≀→< = Nat.≀-trans
  [<β†’<]→≀ {x} {y} h =
    let
      h' : {z : Nat} β†’ z Nat.≀ x β†’ z Nat.≀ y
      h' = Ξ» { {zero} _ β†’ 0≀x; {suc z} β†’ h {z} }
    in h' Nat.≀-refl
  <-wf = Data.Wellfounded.Properties.<-wf

As mentioned above, this representation is rather redundant. We confirm that ordinals are determined by their underlying type and strict order, and can be constructed from the same.

record _≃ₒ_ (Ξ± : Ordinal ℓ₁) (Ξ² : Ordinal β„“β‚‚) : Type (ℓ₁ βŠ” β„“β‚‚) where
  field
    equiv : ⌞ Ξ± ⌟ ≃ ⌞ Ξ² ⌟
    pres-< : βˆ€ {x y} β†’ Ordinal._<_ Ξ± x y ≃ Ordinal._<_ Ξ² (equiv Β· x) (equiv Β· y)
instance
  Funlike-≃ₒ : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ Funlike (Ξ± ≃ₒ Ξ²) ⌞ Ξ± ⌟ Ξ» _ β†’ ⌞ Ξ² ⌟
  Funlike-≃ₒ = record { _Β·_ = fst ∘ _≃ₒ_.equiv }
≃ₒ→≑ : {Ξ± Ξ² : Ordinal β„“} β†’ Ξ± ≃ₒ Ξ² β†’ Ξ± ≑ Ξ²
≃ₒ→≑ {β„“} {Ξ±} {Ξ²} e = p where
Long proof. 
  module Ξ± = Ordinal Ξ±
  module Ξ² = Ordinal Ξ²
  open _≃ₒ_ e
  pβ‚€ : ⌞ Ξ± ⌟ ≑ ⌞ Ξ² ⌟
  pβ‚€ = ua equiv

  p₁ : PathP (Ξ» i β†’ pβ‚€ i β†’ pβ‚€ i β†’ Type β„“) Ξ±._<_ Ξ²._<_
  p₁ = uaβ†’ Ξ» x β†’ uaβ†’ Ξ» y β†’ ua pres-<

  pβ‚‚ : PathP
    (Ξ» i β†’ (x y : pβ‚€ i) β†’
       Ξ£ (Type β„“) Ξ» le β†’ (βˆ€ {z : pβ‚€ i} β†’ p₁ i z x β†’ p₁ i z y) ≃ le)
    (Ξ» x y β†’ x Ξ±.≀ y , prop-ext (hlevel 1) (hlevel 1)
      Ξ±.[<β†’<]→≀ (Ξ» h₁ hβ‚‚ β†’ Ξ±.<→≀→< hβ‚‚ h₁))
    (Ξ» x y β†’ x Ξ².≀ y , prop-ext (hlevel 1) (hlevel 1)
      Ξ².[<β†’<]→≀ (Ξ» h₁ hβ‚‚ β†’ Ξ².<→≀→< hβ‚‚ h₁))
  p₂ = is-prop→pathp (λ i →
    is-contr→is-prop $ Π-is-hlevel 0 λ _ → Π-is-hlevel 0 λ _ →
    is-contr-Ξ£R univalence-identity-system) _ _

  p₃ : PathP (Ξ» i β†’ βˆ€ {x y} β†’ is-prop (fst (pβ‚‚ i x y))) Ξ±.≀-thin Ξ².≀-thin
  p₃ = is-propβ†’pathp (Ξ» _ β†’ hlevel 1) _ _

  pβ‚„ : PathP (Ξ» i β†’ βˆ€ {x} β†’ fst (pβ‚‚ i x x)) Ξ±.≀-refl Ξ².≀-refl
  pβ‚„ = is-propβ†’pathp (Ξ» i β†’ Ξ -is-hlevel' 1 Ξ» x β†’ p₃ i {x} {x}) _ _

  pβ‚… : PathP (Ξ» i β†’ βˆ€ {x y z} β†’ fst (pβ‚‚ i x y) β†’ fst (pβ‚‚ i y z) β†’ fst (pβ‚‚ i x z))
    Ξ±.≀-trans Ξ².≀-trans
  p₅ = is-prop→pathp (λ i →
    Ξ -is-hlevel' 1 Ξ» x β†’ Ξ -is-hlevel' 1 Ξ» y β†’ Ξ -is-hlevel' 1 Ξ» z β†’
    Ξ -is-hlevel 1 Ξ» _ β†’ Ξ -is-hlevel 1 Ξ» _ β†’ p₃ i {x} {z}) _ _

  p₆ : PathP (Ξ» i β†’ βˆ€ {x y} β†’ fst (pβ‚‚ i x y) β†’ fst (pβ‚‚ i y x) β†’ x ≑ y)
    Ξ±.≀-antisym Ξ².≀-antisym
  p₆ = is-prop-i0β†’pathp (
    Ξ -is-hlevel' 1 Ξ» x β†’ Ξ -is-hlevel' 1 Ξ» y β†’
    Ξ -is-hlevel 1 Ξ» _ β†’ Ξ -is-hlevel 1 Ξ» _ β†’ Ξ±.Ob-is-set x y) _ _

  p₇ : PathP (Ξ» i β†’ βˆ€ {x y} β†’ is-prop (p₁ i x y)) Ξ±.<-thin Ξ².<-thin
  p₇ = is-propβ†’pathp (Ξ» _ β†’ hlevel 1) _ _

  pβ‚ˆ : PathP (Ξ» i β†’ βˆ€ {x y} β†’ p₁ i x y β†’ fst (pβ‚‚ i x y)) Ξ±.<→≀ Ξ².<→≀
  pβ‚ˆ = is-propβ†’pathp (Ξ» i β†’
    Ξ -is-hlevel' 1 Ξ» x β†’ Ξ -is-hlevel' 1 Ξ» y β†’ Ξ -is-hlevel 1 Ξ» _ β†’ p₃ i {x} {y}) _ _

  p₉ : PathP (Ξ» i β†’ Wf (p₁ i)) Ξ±.<-wf Ξ².<-wf
  p₉ = is-propβ†’pathp (Ξ» _ β†’ Ξ -is-hlevel 1 Acc-is-prop) _ _

  p : Ξ± ≑ Ξ²
  p i .Ordinal.poset .Poset.Ob = pβ‚€ i
  p i .Ordinal.poset .Poset._≀_ x y = fst (pβ‚‚ i x y)
  p i .Ordinal.poset .Poset.≀-thin {x} {y} = p₃ i {x} {y}
  p i .Ordinal.poset .Poset.≀-refl {x} = pβ‚„ i {x}
  p i .Ordinal.poset .Poset.≀-trans {x} {y} {z} = pβ‚… i {x} {y} {z}
  p i .Ordinal.poset .Poset.≀-antisym {x} {y} = p₆ i {x} {y}
  p i .Ordinal._<_ = p₁ i
  p i .Ordinal.<-thin {x} {y} = p₇ i {x} {y}
  p i .Ordinal.<→≀ {x} {y} = pβ‚ˆ i {x} {y}
  p i .Ordinal.<→≀→< {z} {x} {y} h₁ hβ‚‚ = Equiv.from (snd (pβ‚‚ i x y)) hβ‚‚ {z} h₁
  p i .Ordinal.[<β†’<]→≀ {x} {y} = Equiv.to (snd (pβ‚‚ i x y))
  p i .Ordinal.<-wf = p₉ i
record make-ordinal (β„“ : Level) : Type (lsuc β„“) where
  no-eta-equality
  field
    Ob : Type β„“
    _<_ : Ob β†’ Ob β†’ Type β„“
    <-thin : βˆ€ {x y} β†’ is-prop (x < y)
    <-wf : Wf _<_
    <-trans : βˆ€ {x y z} β†’ x < y β†’ y < z β†’ x < z
    <-extensional : βˆ€ {x y} β†’ (βˆ€ {z} β†’ (z < x β†’ z < y) Γ— (z < y β†’ z < x)) β†’ x ≑ y

  to-ordinal : Ordinal β„“
  to-ordinal = record where
    poset = record where
      Ob = Ob
      _≀_ x y = βˆ€ {z} β†’ z < x β†’ z < y
      ≀-thin = Ξ -is-hlevel' 1 Ξ» _ β†’ Ξ -is-hlevel 1 Ξ» _ β†’ <-thin
      ≀-refl = id
      ≀-trans h₁ hβ‚‚ = hβ‚‚ ∘ h₁
      ≀-antisym h₁ hβ‚‚ = <-extensional (h₁ , hβ‚‚)
    _<_ = _<_
    <-thin = <-thin
    <→≀ x<y z<x = <-trans z<x x<y
    <→≀→< x<y y≀z = y≀z x<y
    [<β†’<]→≀ = id
    <-wf = <-wf

The _≃ₒ_ relation in fact defines an identity system, but we’ll prove that later. For now, we show it’s reflexive, symmetric, and transitive.

≃ₒ-refl : {Ξ± : Ordinal β„“} β†’ Ξ± ≃ₒ Ξ±
≃ₒ-refl = record { equiv = id≃ ; pres-< = id≃ }

≃ₒ-trans : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {Ξ³ : Ordinal ℓ₃}
  β†’ Ξ± ≃ₒ Ξ² β†’ Ξ² ≃ₒ Ξ³ β†’ Ξ± ≃ₒ Ξ³
≃ₒ-trans e₁ eβ‚‚ =
  let module e₁ = _≃ₒ_ e₁; module eβ‚‚ = _≃ₒ_ eβ‚‚
  in record { equiv = e₁.equiv βˆ™e eβ‚‚.equiv ; pres-< = e₁.pres-< βˆ™e eβ‚‚.pres-< }

≃ₒ-sym : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ Ξ± ≃ₒ Ξ² β†’ Ξ² ≃ₒ Ξ±
≃ₒ-sym {_} {_} {Ξ±} {Ξ²} e =
  let
    open _≃ₒ_ e
    equiv' = equiv e⁻¹
    counit = equiv→counit (snd equiv)
  in record {
    equiv = equiv';
    pres-< = Ξ» {x} {y} β†’ transport
      (Ξ» i β†’
        Ordinal._<_ Ξ² (counit x i) (counit y i) ≃
        Ordinal._<_ Ξ± (fst equiv' x) (fst equiv' y))
    (pres-< {equiv' · x} {equiv' · y} e⁻¹)
  }

SubordinalsπŸ”—

Given any element of an ordinal, the elements below it form an ordinal of their own.

module _ (Ξ± : Ordinal β„“) (a : ⌞ Ξ± ⌟) where
  open Ordinal Ξ±
  Subordinal : Ordinal β„“
  Subordinal .Ordinal.poset = Subposet poset Ξ» x β†’ el (x < a) <-thin
  Subordinal .Ordinal._<_ (x , _) (y , _) = x < y
  Subordinal .Ordinal.<-thin = <-thin
  Subordinal .Ordinal.<→≀ = <→≀
  Subordinal .Ordinal.<→≀→< = <→≀→<
  Subordinal .Ordinal.[<β†’<]→≀ {x , x<a} {y , y<a} h =
    [<β†’<]→≀ (Ξ» {z} z<x β†’ h {z , <-trans z<x x<a} z<x)
  Subordinal .Ordinal.<-wf (x , x<a) = Wf-induction _<_ <-wf
    (Ξ» x β†’ (x<a : x < a)
      β†’ Acc (Ξ» (x y : Ξ£ ⌞ Ξ± ⌟ (_< a)) β†’ fst x < fst y) (x , x<a))
    (Ξ» x ih x<a β†’ acc Ξ» (y , y<a) y<x β†’ ih y y<x y<a)
    x x<a

SimulationsπŸ”—

The correct notion of map between ordinals, called a simulation, is a strictly monotone function that induces an equivalence on subordinals.

record is-simulation (Ξ± : Ordinal ℓ₁) (Ξ² : Ordinal β„“β‚‚)
  (f : ⌞ Ξ± ⌟ β†’ ⌞ Ξ² ⌟) : Type (ℓ₁ βŠ” β„“β‚‚) where
  no-eta-equality
  private
    module Ξ± = Ordinal Ξ±
    module Ξ² = Ordinal Ξ²
  field
    pres-< : βˆ€ {x y} β†’ x Ξ±.< y β†’ f x Ξ².< f y
  segment : (x : Ξ±.Ob) β†’ ⌞ Subordinal Ξ± x ⌟ β†’ ⌞ Subordinal Ξ² (f x) ⌟
  segment x (y , y<x) = f y , pres-< y<x
  field
    segment-is-equiv : βˆ€ {x} β†’ is-equiv (segment x)
  sim : βˆ€ {x y} β†’ y Ξ².< f x β†’ ⌞ Ξ± ⌟
  sim h = fst (equiv→inverse segment-is-equiv (_ , h))
  simulates : βˆ€ {x y} β†’ (y<fx : y Ξ².< f x) β†’ f (sim y<fx) ≑ y
  simulates h = ap fst (equiv→counit segment-is-equiv (_ , h))
  sim-< : βˆ€ {x y} β†’ (y<fx : y Ξ².< f x) β†’ sim y<fx Ξ±.< x
  sim-< h = snd (equiv→inverse segment-is-equiv (_ , h))

Simulations are injective, and monotone in every reasonable sense.

  pres-≀ : βˆ€ {x y} β†’ x Ξ±.≀ y β†’ f x Ξ².≀ f y
  pres-≀ {x} {y} x≀y = Ξ².[<β†’<]→≀ Ξ» {z} z<fx β†’
    transport (Ξ» i β†’ simulates z<fx i Ξ².< f y) (pres-< (Ξ±.<→≀→< (sim-< z<fx) x≀y))

  reflect-≀ : βˆ€ {x y} β†’ f x Ξ².≀ f y β†’ x Ξ±.≀ y
  reflect-≀ = go (Ξ±.<-wf _) (Ξ±.<-wf _) where
    go : βˆ€ {x y} β†’ Acc Ξ±._<_ x β†’ Acc Ξ±._<_ y β†’ f x Ξ².≀ f y β†’ x Ξ±.≀ y
    go {x} {y} (acc hx) (acc hy) fx≀fy =
      Ξ±.[<β†’<]→≀ Ξ» {z} z<x β†’
      let
        fz<fx = pres-< z<x
        fz<fy = Ξ².<→≀→< fz<fx fx≀fy
        w = sim fz<fy
        w<y = sim-< fz<fy
        fw≑fz = simulates fz<fy
        w≀z = go (hy w w<y) (hx z z<x) (Ξ².≀-refl' fw≑fz)
        z≀w = go (hx z z<x) (hy w w<y) (Ξ².≀-refl' (sym fw≑fz))
        w≑z = Ξ±.≀-antisym w≀z z≀w
      in transport (Ξ» i β†’ w≑z i Ξ±.< y) w<y

  has-injective : injective f
  has-injective p = Ξ±.≀-antisym
    (reflect-≀ (Ξ².≀-refl' p))
    (reflect-≀ (Ξ².≀-refl' (sym p)))

  has-is-embedding : is-embedding f
  has-is-embedding = injective→is-embedding β.Ob-is-set f has-injective

  reflect-< : βˆ€ {x y} β†’ f x Ξ².< f y β†’ x Ξ±.< y
  reflect-< {x} {y} fx<fy =
    transport (Ξ» i β†’ has-injective (simulates fx<fy) i Ξ±.< y) (sim-< fx<fy)

  Subordinal-≃ : (x : Ξ±.Ob) β†’ Subordinal Ξ± x ≃ₒ Subordinal Ξ² (f x)
  Subordinal-≃ x = record where
    equiv = segment x , segment-is-equiv
    pres-< = prop-ext Ξ±.<-thin Ξ².<-thin pres-< reflect-<
is-simulation-is-prop : βˆ€ {Ξ± Ξ² f} β†’ is-prop (is-simulation {ℓ₁} {β„“β‚‚} Ξ± Ξ² f)
is-simulation-is-prop {_} {_} {Ξ±} {Ξ²} {f} s₁ sβ‚‚ = p where
  open is-simulation
  p₁ : βˆ€ {x y} β†’ pres-< s₁ {x} {y} ≑ pres-< sβ‚‚ {x} {y}
  p₁ = hlevel 1 _ _
  pβ‚‚ : βˆ€ {x} β†’ PathP
    (Ξ» i β†’ is-equiv {A = ⌞ Subordinal Ξ± x ⌟} {B = ⌞ Subordinal Ξ² (f x) ⌟}
      Ξ» (y , y<x) β†’ f y , p₁ i y<x)
    (segment-is-equiv s₁ {x})
    (segment-is-equiv sβ‚‚ {x})
  p₂ = is-prop→pathp (λ _ → is-equiv-is-prop _) _ _
  p : s₁ ≑ sβ‚‚
  p i .pres-< = p₁ i
  p i .segment-is-equiv = pβ‚‚ i

instance
  H-Level-is-simulation
    : βˆ€ {n} {β„“} {Ξ± Ξ² : Ordinal β„“} {f} β†’ H-Level (is-simulation Ξ± Ξ² f) (suc n)
  H-Level-is-simulation = prop-instance is-simulation-is-prop

If a simulation is also an equivalence, it forces the ordinals to be equal.

is-simulationβ†’is-equiv→≃ₒ : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {f : ⌞ Ξ± ⌟ β†’ ⌞ Ξ² ⌟}
  (sim : is-simulation Ξ± Ξ² f) (e : is-equiv f) β†’ Ξ± ≃ₒ Ξ²
is-simulationβ†’is-equiv→≃ₒ _ e ._≃ₒ_.equiv = _ , e
is-simulationβ†’is-equiv→≃ₒ {_} {_} {Ξ±} {Ξ²} sim _ ._≃ₒ_.pres-< = prop-ext
  (Ordinal.<-thin Ξ±) (Ordinal.<-thin Ξ²)
  (is-simulation.pres-< sim) (is-simulation.reflect-< sim)

OrderingπŸ”—

Intriguingly, simulations are unique.

simulation-unique : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {f g : ⌞ Ξ± ⌟ β†’ ⌞ Ξ² ⌟} β†’
  is-simulation Ξ± Ξ² f β†’ is-simulation Ξ± Ξ² g β†’ f ≑ g
simulation-unique {_} {_} {Ξ±} {Ξ²} {f} {g} f-sim g-sim =
  let
    module Ξ± = Ordinal Ξ±
    module Ξ² = Ordinal Ξ²
    open is-simulation
  in ext $ Wf-induction Ξ±._<_ Ξ±.<-wf (Ξ» x β†’ f x ≑ g x) Ξ» x ih β†’
    Ξ².≀-antisym
      (Ξ².[<β†’<]→≀ Ξ» z<fx β†’
        subst (Ξ» z β†’ z Ξ².< g x)
          (sym (ih (sim f-sim z<fx) (sim-< f-sim z<fx)) βˆ™ simulates f-sim z<fx)
          (pres-< g-sim (sim-< f-sim z<fx)))
      (Ξ².[<β†’<]→≀ Ξ» z<gx β†’
        subst (Ξ» z β†’ z Ξ².< f x)
          (ih (sim g-sim z<gx) (sim-< g-sim z<gx) βˆ™ simulates g-sim z<gx)
          (pres-< f-sim (sim-< g-sim z<gx)))

So they induce an ordering on ordinals.

_≀ₒ_ : (Ξ± : Ordinal ℓ₁) (Ξ² : Ordinal β„“β‚‚) β†’ Type (ℓ₁ βŠ” β„“β‚‚)
Ξ± ≀ₒ Ξ² = Ξ£ (⌞ Ξ± ⌟ β†’ ⌞ Ξ² ⌟) (is-simulation Ξ± Ξ²)

≀ₒ-thin : {ℓ₁ β„“β‚‚ : Level} {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ is-prop (Ξ± ≀ₒ Ξ²)
≀ₒ-thin (_ , f-sim) (_ , g-sim) =
  Ξ£-path (simulation-unique f-sim g-sim) (is-simulation-is-prop _ _)

≀ₒ-refl : {Ξ± : Ordinal β„“} β†’ Ξ± ≀ₒ Ξ±
≀ₒ-refl = id , record { pres-< = id ; segment-is-equiv = id-equiv }

≀ₒ-trans : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {Ξ³ : Ordinal ℓ₃}
  β†’ Ξ± ≀ₒ Ξ² β†’ Ξ² ≀ₒ Ξ³ β†’ Ξ± ≀ₒ Ξ³
≀ₒ-trans (f , f-sim) (g , g-sim) = g ∘ f , record where
  open is-simulation
  pres-< = pres-< g-sim ∘ pres-< f-sim
  segment-is-equiv = ∘-is-equiv (segment-is-equiv g-sim) (segment-is-equiv f-sim)

≀ₒ-antisym : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ Ξ± ≀ₒ Ξ² β†’ Ξ² ≀ₒ Ξ± β†’ Ξ± ≃ₒ Ξ²
≀ₒ-antisym {_} {_} {Ξ±} {Ξ²} α≀β β≀α =
  is-simulationβ†’is-equiv→≃ₒ (snd α≀β)
  $ is-iso→is-equiv
  $ iso (fst β≀α)
    (happly (ap fst (≀ₒ-thin (≀ₒ-trans β≀α α≀β) ≀ₒ-refl)))
    (happly (ap fst (≀ₒ-thin (≀ₒ-trans α≀β β≀α) ≀ₒ-refl)))

≃ₒ→≀ₒ : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ Ξ± ≃ₒ Ξ² β†’ Ξ± ≀ₒ Ξ²
≃ₒ→≀ₒ e =
  let open _≃ₒ_ e
  in fst equiv , record {
    pres-< = fst pres-<;
    segment-is-equiv = snd (Ξ£-ap equiv Ξ» _ β†’ pres-<)
  }

Ordinal-poset : (β„“ : Level) β†’ Poset (lsuc β„“) β„“
Ordinal-poset β„“ .Poset.Ob = Ordinal β„“
Ordinal-poset β„“ .Poset._≀_ = _≀ₒ_
Ordinal-poset β„“ .Poset.≀-thin = ≀ₒ-thin
Ordinal-poset β„“ .Poset.≀-refl = ≀ₒ-refl
Ordinal-poset β„“ .Poset.≀-trans = ≀ₒ-trans
Ordinal-poset β„“ .Poset.≀-antisym h₁ hβ‚‚ = ≃ₒ→≑ (≀ₒ-antisym h₁ hβ‚‚)

In particular, the type of ordinals is a set, and _≃ₒ_ forms an identity system.

Ordinal-is-set : is-set (Ordinal β„“)
Ordinal-is-set {β„“} = Poset.Ob-is-set (Ordinal-poset β„“)

private unquoteDecl ≃ₒ-path = declare-record-path ≃ₒ-path (quote _≃ₒ_)

≃ₒ-thin : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ is-prop (Ξ± ≃ₒ Ξ²)
≃ₒ-thin {_} {_} {Ξ±} {Ξ²} = retractβ†’is-prop
  {A = (Ξ± ≀ₒ Ξ²) Γ— (Ξ² ≀ₒ Ξ±)}
  (Ξ» (α≀β , β≀α) β†’ ≀ₒ-antisym α≀β β≀α)
  (Ξ» e β†’ ≃ₒ→≀ₒ e , ≃ₒ→≀ₒ (≃ₒ-sym e))
  (Ξ» e β†’ ≃ₒ-path (ext Ξ» x β†’ refl))
  (Γ—-is-hlevel 1 ≀ₒ-thin ≀ₒ-thin)

≃ₒ-identity-system : is-identity-system {A = Ordinal β„“} _≃ₒ_ Ξ» _ β†’ ≃ₒ-refl
≃ₒ-identity-system = set-identity-system {r = Ξ» _ β†’ ≃ₒ-refl} (Ξ» _ _ β†’ ≃ₒ-thin) ≃ₒ→≑
instance
  H-Level-Ordinal
    : βˆ€ {n} {β„“} β†’ H-Level (Ordinal β„“) (suc (suc n))
  H-Level-Ordinal = basic-instance 2 Ordinal-is-set

  H-Level-≃ₒ
    : βˆ€ {n ℓ₁ β„“β‚‚} {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ H-Level (Ξ± ≃ₒ Ξ²) (suc n)
  H-Level-≃ₒ = basic-instance 1 ≃ₒ-thin

We conclude with the ways in which subordinals interact with the order.

module _ {Ξ± : Ordinal β„“} {x : ⌞ Ξ± ⌟} {y : ⌞ Subordinal Ξ± x ⌟} where
  open Ordinal Ξ±
  Subsubordinal : Subordinal (Subordinal Ξ± x) y ≃ₒ Subordinal Ξ± (fst y)
  Subsubordinal ._≃ₒ_.equiv = Isoβ†’Equiv
    $ (Ξ» ((z , z<x) , z<y) β†’ z , z<y)
    , iso
      (Ξ» (z , z<y) β†’ (z , <-trans z<y (snd y)) , z<y)
      (Ξ» _ β†’ refl)
      (Ξ» ((z , z<x) , z<y) β†’ Ξ£-pathp (Ξ£-pathp refl (<-thin _ _)) refl)
  Subsubordinal ._≃ₒ_.pres-< = id≃

Subordinal-≀ₒ : {Ξ± : Ordinal ℓ₁} {x : ⌞ Ξ± ⌟} β†’ Subordinal Ξ± x ≀ₒ Ξ±
Subordinal-≀ₒ {Ξ± = Ξ±} {x} = fst , record where
  pres-< = id
  segment-is-equiv {y} = Subsubordinal {Ξ± = Ξ±} {x} {y} ._≃ₒ_.equiv .snd 

is-subordinal-simulationβ†’is-identity : βˆ€ {Ξ± : Ordinal β„“} {x y f}
  β†’ is-simulation (Subordinal Ξ± x) (Subordinal Ξ± y) f
  β†’ fst ∘ f ≑ fst
is-subordinal-simulation→is-identity {α = α} {x} {y} {f} sim =
  simulation-unique (snd (≀ₒ-trans (f , sim) Subordinal-≀ₒ)) (snd Subordinal-≀ₒ)

Subordinal-preserves-≀ₒ : {Ξ± : Ordinal β„“} {x y : ⌞ Ξ± ⌟}
  β†’ Ordinal._≀_ Ξ± x y β†’ Subordinal Ξ± x ≀ₒ Subordinal Ξ± y
Subordinal-preserves-≀ₒ {Ξ± = Ξ±} {x} {y} h =
  let open Ordinal Ξ±
  in (Ξ» (z , z<x) β†’ z , <→≀→< z<x h) , record where
    pres-< = id
    segment-is-equiv {z , z<x} = is-iso→is-equiv record where
      from ((w , w<y) , w<z) = (w , <-trans w<z z<x) , w<z
      rinv _ = Ξ£-path (Ξ£-path refl (<-thin _ _)) (<-thin _ _)
      linv _ = Ξ£-path (Ξ£-path refl (<-thin _ _)) (<-thin _ _)

Subordinal-reflects-≀ₒ : {Ξ± : Ordinal β„“} {x y : ⌞ Ξ± ⌟}
  β†’ Subordinal Ξ± x ≀ₒ Subordinal Ξ± y β†’ Ordinal._≀_ Ξ± x y
Subordinal-reflects-≀ₒ {Ξ± = Ξ±} {x} {y} h =
  let open Ordinal Ξ±
  in [<β†’<]→≀ Ξ» {z} z<x β†’ subst (_< y)
    (happly (is-subordinal-simulation→is-identity (snd h)) (z , z<x))
    (snd (h Β· (z , z<x)))

Subordinal-injective : {Ξ± : Ordinal β„“} {x y : ⌞ Ξ± ⌟}
  β†’ Subordinal Ξ± x ≃ₒ Subordinal Ξ± y β†’ x ≑ y
Subordinal-injective {Ξ± = Ξ±} e = Ordinal.≀-antisym Ξ±
  (Subordinal-reflects-≀ₒ (≃ₒ→≀ₒ e))
  (Subordinal-reflects-≀ₒ (≃ₒ→≀ₒ (≃ₒ-sym e)))

The ordinal of ordinalsπŸ”—

The collection of ordinals is itself well-ordered, with the strict inequality coming from the notion of subordinal. Induction over this ordering is known as transfinite induction.

_<β‚’_ : Ordinal ℓ₁ β†’ Ordinal β„“β‚‚ β†’ Type (ℓ₁ βŠ” β„“β‚‚)
Ξ± <β‚’ Ξ² = Ξ£ ⌞ Ξ² ⌟ Ξ» x β†’ Ξ± ≃ₒ Subordinal Ξ² x

<β‚’-thin : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ is-prop (Ξ± <β‚’ Ξ²)
<β‚’-thin {ℓ₁} {β„“β‚‚} {Ξ±} {Ξ²} (x , e₁) (y , eβ‚‚) =
  Ξ£-path (Subordinal-injective (≃ₒ-trans (≃ₒ-sym e₁) eβ‚‚)) (≃ₒ-thin _ _)

<ₒ→≀ₒ : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} β†’ Ξ± <β‚’ Ξ² β†’ Ξ± ≀ₒ Ξ²
<ₒ→≀ₒ (x , e) = ≀ₒ-trans (≃ₒ→≀ₒ e) Subordinal-≀ₒ

≃ₒ→<β‚’β†’<β‚’ : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {Ξ³ : Ordinal ℓ₃}
  β†’ Ξ± ≃ₒ Ξ² β†’ Ξ² <β‚’ Ξ³ β†’ Ξ± <β‚’ Ξ³
≃ₒ→<β‚’β†’<β‚’ e₁ (x , eβ‚‚) = x , ≃ₒ-trans e₁ eβ‚‚

<ₒ→≀ₒ→<β‚’ : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {Ξ³ : Ordinal ℓ₃}
  β†’ Ξ± <β‚’ Ξ² β†’ Ξ² ≀ₒ Ξ³ β†’ Ξ± <β‚’ Ξ³
<ₒ→≀ₒ→<β‚’ (x , e) (f , sim) = f x , ≃ₒ-trans e (is-simulation.Subordinal-≃ sim x)

<β‚’-trans : {Ξ± : Ordinal ℓ₁} {Ξ² : Ordinal β„“β‚‚} {Ξ³ : Ordinal ℓ₃}
  β†’ Ξ± <β‚’ Ξ² β†’ Ξ² <β‚’ Ξ³ β†’ Ξ± <β‚’ Ξ³
<β‚’-trans h₁ hβ‚‚ = <ₒ→≀ₒ→<β‚’ h₁ (<ₒ→≀ₒ hβ‚‚)

<β‚’-wf : Wf (_<β‚’_ {β„“} {β„“})
<β‚’-wf {β„“} Ξ± = acc Ξ» Ξ² Ξ²<Ξ± β†’ go Ξ² Ξ²<Ξ± (<-wf (fst Ξ²<Ξ±)) where
  open Ordinal Ξ±
  go : (Ξ² : Ordinal β„“) β†’ (Ξ²<Ξ± : Ξ² <β‚’ Ξ±) β†’ Acc _<_ (fst Ξ²<Ξ±) β†’ Acc _<β‚’_ Ξ²
  go Ξ² Ξ²<Ξ± (acc h) = acc Ξ» Ξ³ Ξ³<Ξ² β†’ go Ξ³
    (<β‚’-trans Ξ³<Ξ² Ξ²<Ξ±)
    (h _ (snd (_≃ₒ_.equiv (snd Ξ²<Ξ±) Β· fst Ξ³<Ξ²)))

Subordinal-preserves-<β‚’ : {Ξ± : Ordinal β„“} {x y : ⌞ Ξ± ⌟}
  β†’ Ordinal._<_ Ξ± x y β†’ Subordinal Ξ± x <β‚’ Subordinal Ξ± y
Subordinal-preserves-<β‚’ {Ξ± = Ξ±} {x} {y} x<y = (x , x<y) , ≃ₒ-sym Subsubordinal

Subordinal-reflects-<β‚’ : {Ξ± : Ordinal β„“} {x y : ⌞ Ξ± ⌟}
  β†’ Subordinal Ξ± x <β‚’ Subordinal Ξ± y β†’ Ordinal._<_ Ξ± x y
Subordinal-reflects-<β‚’ {Ξ± = Ξ±} {x} {y} ((z , z<y) , e) =
  let
    x≑z : x ≑ z
    x≑z = Subordinal-injective (≃ₒ-trans e Subsubordinal)
  in transport (Ξ» i β†’ Ordinal._<_ Ξ± (x≑z (~ i)) y) z<y

[<β‚’β†’<β‚’]→≀ₒ : {Ξ± Ξ² : Ordinal β„“} β†’ (βˆ€ {Ξ³ : Ordinal β„“} β†’ Ξ³ <β‚’ Ξ± β†’ Ξ³ <β‚’ Ξ²) β†’ Ξ± ≀ₒ Ξ²
[<β‚’β†’<β‚’]→≀ₒ {Ξ± = Ξ±} {Ξ²} h =
  let
    f : ⌞ Ξ± ⌟ β†’ ⌞ Ξ² ⌟
    f x = fst (h (x , ≃ₒ-refl))
    hf : βˆ€ x β†’ Subordinal Ξ± x ≃ₒ Subordinal Ξ² (f x)
    hf x = snd (h (x , ≃ₒ-refl))
  in f , record where
    open Ordinal Ξ²
    pres-< {x} {y} h = Subordinal-reflects-<β‚’
      (<ₒ→≀ₒ→<β‚’
        (≃ₒ→<β‚’β†’<β‚’ (≃ₒ-sym (hf x)) (Subordinal-preserves-<β‚’ h))
        (≃ₒ→≀ₒ (hf y)))
    segment-is-hf : βˆ€ x β†’ Path (⌞ Subordinal Ξ± x ⌟ β†’ ⌞ Subordinal Ξ² (f x) ⌟)
      (Ξ» (y , y<x) β†’ f y , pres-< y<x)
      (hf x ._≃ₒ_.equiv .fst)
    segment-is-hf x = funext Ξ» (y , y<x) β†’ Ξ£-path
      (Subordinal-injective
      $ ≃ₒ-trans (≃ₒ-sym (hf y))
      $ ≃ₒ-trans (≃ₒ-sym Subsubordinal)
      $ ≃ₒ-trans (is-simulation.Subordinal-≃ (snd (≃ₒ→≀ₒ (hf x))) (y , y<x))
      $ Subsubordinal)
      (<-thin _ _)
    segment-is-equiv {x} =
      transport (Ξ» i β†’ is-equiv (segment-is-hf x (~ i))) (hf x ._≃ₒ_.equiv .snd)

We have everything we need to assemble the ordinal of ordinals, but the construction is complicated by the need to shift universe levels.

Ord : (β„“ : Level) β†’ Ordinal (lsuc β„“)
Ord β„“ = record where
  poset = record where
    Ob = Ordinal β„“
    _≀_ Ξ± Ξ² = Lift _ (Ξ± ≀ₒ Ξ²)
    ≀-thin (lift h₁) (lift hβ‚‚) = ap lift (≀ₒ-thin h₁ hβ‚‚)
    ≀-refl = lift ≀ₒ-refl
    ≀-trans (lift h₁) (lift hβ‚‚) = lift (≀ₒ-trans h₁ hβ‚‚)
    ≀-antisym (lift h₁) (lift hβ‚‚) = ≃ₒ→≑ (≀ₒ-antisym h₁ hβ‚‚)
  _<_ Ξ± Ξ² = Lift _ (Ξ± <β‚’ Ξ²)
  <-thin (lift h₁) (lift hβ‚‚) = ap lift (<β‚’-thin h₁ hβ‚‚)
  <-wf = Wf-induction _<β‚’_ <β‚’-wf (Acc _<_) Ξ» Ξ± ih β†’ acc (Ξ» y (lift h) β†’ ih y h)
  <→≀→< (lift h₁) (lift hβ‚‚) = lift (<ₒ→≀ₒ→<β‚’ h₁ hβ‚‚)
  [<β†’<]→≀ h = lift ([<β‚’β†’<β‚’]→≀ₒ (Ξ» h' β†’ lower (h (lift h'))))
  <→≀ (lift h) = lift (<ₒ→≀ₒ h)

Subordinals of OrdπŸ”—

Every ordinal at level β„“ is a subordinal of Ord.

Subordinal-Ord : {Ξ± : Ordinal β„“} β†’ Subordinal (Ord β„“) Ξ± ≃ₒ Ξ±
Subordinal-Ord {Ξ± = Ξ±} = record where
  equiv = (λ (_ , lift (x , _)) → x) , is-iso→is-equiv record where
    from x = Subordinal Ξ± x , lift (x , ≃ₒ-refl)
    rinv x = refl
    linv (Ξ² , lift (x , e)) =
      Ξ£-pathp (sym (≃ₒ→≑ e)) (apd (Ξ» _ β†’ lift)
        (Ξ£-pathp refl (is-propβ†’pathp (Ξ» _ β†’ ≃ₒ-thin) _ _)))
  pres-< {β₁ , lift (x₁ , e₁)} {Ξ²β‚‚ , lift (xβ‚‚ , eβ‚‚)} = prop-ext
    (Lift-is-hlevel 1 <β‚’-thin) (Ordinal.<-thin Ξ±)
    (Ξ» h β†’
      Subordinal-reflects-<β‚’ (≃ₒ→<β‚’β†’<β‚’ (≃ₒ-sym e₁) (<ₒ→≀ₒ→<β‚’ (lower h) (≃ₒ→≀ₒ eβ‚‚))))
    (Ξ» h β†’
      lift (≃ₒ→<β‚’β†’<β‚’ e₁ (<ₒ→≀ₒ→<β‚’ (Subordinal-preserves-<β‚’ h) (≃ₒ→≀ₒ (≃ₒ-sym eβ‚‚)))))

<β‚’-Ord : (Ξ± : Ordinal β„“) β†’ Ξ± <β‚’ Ord β„“
<β‚’-Ord Ξ± = Ξ± , ≃ₒ-sym Subordinal-Ord

As a consequence, Ord is a large ordinal β€” it is not equivalent to any ordinal in the previous universe. In naΓ―ve set theory, this leads to the Burali-Forti paradox.

Ord-large : (β„“ : Level) β†’ Β¬ Ξ£ (Ordinal β„“) (Ord β„“ ≃ₒ_)
Ord-large β„“ (Ξ© , e) = Ordinal.<-irrefl (Ord β„“) (lift Ξ©<Ξ©) where
  Ξ©<Ξ© : Ξ© <β‚’ Ξ©
  Ξ©<Ξ© = <ₒ→≀ₒ→<β‚’ (<β‚’-Ord Ξ©) (≃ₒ→≀ₒ e)