Martin Escardo, 29 June 2018

The type Ordinals of ordinals in a universe U, and the subtype Ordinalsᵀ of
ordinals with a top element.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

open import SpartanMLTT

open import OrdinalNotions

open import UF-Base
open import UF-FunExt
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-Embeddings

module OrdinalsType where

\end{code}

An ordinal is a type equipped with ordinal structure. Such a type is
automatically a set.

\begin{code}

OrdinalStructure : 𝓤 ̇  𝓤  ̇
OrdinalStructure {𝓤} X = Σ _<_  (X  X  𝓤 ̇ ) , (is-well-order _<_)

Ordinal :  𝓤  𝓤  ̇
Ordinal 𝓤 = Σ X  𝓤 ̇ , OrdinalStructure X

Ord = Ordinal 𝓤₀

\end{code}

NB. Perhaps we will eventually need to have two parameters 𝓤 (the
universe where the underlying type X lives) and 𝓥 (the universe where
_<_ takes values in) for Ordinal.

Ordinals are ranged over by α,β,γ.

The underlying type of an ordinal (which happens to be necessarily a
set):

\begin{code}

⟨_⟩ : Ordinal 𝓤  𝓤 ̇
 X , _<_ , o  = X

structure : (α : Ordinal 𝓤)  OrdinalStructure  α 
structure (X , s) = s

underlying-order : (α : Ordinal 𝓤)   α    α   𝓤 ̇
underlying-order (X , _<_ , o) = _<_

underlying-weak-order : (α : Ordinal 𝓤)   α    α   𝓤 ̇
underlying-weak-order α x y = ¬ (underlying-order α y x)

underlying-porder : (α : Ordinal 𝓤)   α    α   𝓤 ̇
underlying-porder (X , _<_ , o) = extensional-po _<_

syntax underlying-order       α x y = x ≺⟨ α  y
syntax underlying-weak-order  α x y = x ≾⟨ α  y
syntax underlying-porder      α x y = x ≼⟨ α  y

is-well-ordered : (α : Ordinal 𝓤)  is-well-order (underlying-order α)
is-well-ordered (X , _<_ , o) = o

Prop-valuedness : (α : Ordinal 𝓤)  is-prop-valued (underlying-order α)
Prop-valuedness α = prop-valuedness (underlying-order α) (is-well-ordered α)

Transitivity : (α : Ordinal 𝓤)  is-transitive (underlying-order α)
Transitivity α = transitivity (underlying-order α) (is-well-ordered α)

Well-foundedness : (α : Ordinal 𝓤) (x :  α )  is-accessible (underlying-order α) x
Well-foundedness α = well-foundedness (underlying-order α) (is-well-ordered α)

Transfinite-induction : (α : Ordinal 𝓤)
                       (P :  α   𝓦 ̇ )
                       ((x :  α )  ((y :  α )  y ≺⟨ α  x  P y)  P x)
                       (x :  α )  P x
Transfinite-induction α = transfinite-induction
                           (underlying-order α)
                           (Well-foundedness α)

Extensionality : (α : Ordinal 𝓤)  is-extensional (underlying-order α)
Extensionality α = extensionality (underlying-order α) (is-well-ordered α)

underlying-type-is-set : FunExt
                        (α : Ordinal 𝓤)
                        is-set  α 
underlying-type-is-set fe α =
 extensionally-ordered-types-are-sets
  (underlying-order α)
  fe
  (Prop-valuedness α)
  (Extensionality α)

has-bottom : Ordinal 𝓤  𝓤 ̇
has-bottom α = Σ    α  , ((x :  α )   ≼⟨ α  x)

having-bottom-is-prop : Fun-Ext  (α : Ordinal 𝓤)  is-prop (has-bottom α)
having-bottom-is-prop fe α ( , l) (⊥' , l') =
  to-subtype-≡
     _  Π₃-is-prop fe  x y _  Prop-valuedness α y x))
    (Extensionality α  ⊥' (l ⊥') (l' ))

\end{code}

TODO. We should add further properties of the order from the module
OrdinalNotions. For the moment, we add this:

\begin{code}

irrefl : (α : Ordinal 𝓤) (x :  α )  ¬(x ≺⟨ α  x)
irrefl α x = irreflexive (underlying-order α) x (Well-foundedness α x)

\end{code}

Characterization of equality of ordinals using the structure identity
principle:

\begin{code}

open import UF-Equiv
open import UF-Univalence

Ordinal-≡ : FunExt
           is-univalent 𝓤
           (α β : Ordinal 𝓤)
           (α  β)
           (Σ f  ( α    β ) ,
                 is-equiv f
               × ((λ x x'  x ≺⟨ α  x')   x x'  f x ≺⟨ β  f x')))
Ordinal-≡ {𝓤} fe = generalized-metric-space.characterization-of-M-≡ (𝓤 ̇ )
                     _  is-well-order)
                     X _<_  being-well-order-is-prop _<_ fe)
 where
  open import UF-SIP-Examples

\end{code}

Often it is convenient to work with the following alternative notion
of ordinal equivalence, which we take as the official one:

\begin{code}

is-order-preserving : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
                     ( α    β )  𝓤  𝓥 ̇
is-order-preserving α β f = (x y :  α )  x ≺⟨ α  y  f x ≺⟨ β  f y

is-order-equiv : (α : Ordinal 𝓤) (β : Ordinal 𝓥)  ( α    β )  𝓤  𝓥 ̇
is-order-equiv α β f = is-order-preserving α β f
                     × (Σ e  is-equiv f , is-order-preserving β α (inverse f e))

is-order-reflecting : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
                     ( α    β )  𝓤  𝓥 ̇
is-order-reflecting α β f = (x y :  α )  f x ≺⟨ β  f y  x ≺⟨ α  y

order-equiv-criterion : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f :  α    β )
                       is-equiv f
                       is-order-preserving α β f
                       is-order-reflecting α β f
                       is-order-equiv α β f
order-equiv-criterion α β f e p r = p , e , q
 where
  g :  β    α 
  g = inverse f e

  q : is-order-preserving β α g
  q x y l = m
   where
    l' : f (g x) ≺⟨ β  f (g y)
    l' = transport₂  x y  x ≺⟨ β  y)
           ((inverses-are-sections f e x)⁻¹) ((inverses-are-sections f e y)⁻¹) l

    s : f (g x) ≺⟨ β  f (g y)  g x ≺⟨ α  g y
    s = r (g x) (g y)

    m : g x ≺⟨ α  g y
    m = s l'


order-equiv-criterion-converse : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f :  α    β )
                                is-order-equiv α β f
                                is-order-reflecting α β f
order-equiv-criterion-converse α β f (p , e , q) x y l = r
 where
  g :  β    α 
  g = inverse f e

  s : g (f x) ≺⟨ α  g (f y)
  s = q (f x) (f y) l

  r : x ≺⟨ α  y
  r = transport₂  x y  x ≺⟨ α  y)
       (inverses-are-retractions f e x) (inverses-are-retractions f e y) s

_≃ₒ_ : Ordinal 𝓤  Ordinal 𝓥  𝓤  𝓥 ̇
α ≃ₒ β = Σ f  ( α    β ) , is-order-equiv α β f

\end{code}

See the module  for a proof that α ≃ₒ β is
canonically equivalent to α ≡ β. (For historical reasons, that proof
doesn't use the structure identity principle.)

\begin{code}

≃ₒ-refl : (α : Ordinal 𝓤)  α ≃ₒ α
≃ₒ-refl α = id ,  x y  id) , id-is-equiv  α  ,  x y  id)

≃ₒ-sym :  {𝓤} {𝓥} (α : Ordinal 𝓤) (β : Ordinal 𝓥 )
        α ≃ₒ β  β ≃ₒ α
≃ₒ-sym α β (f , p , e , q) = inverse f e , q , inverses-are-equivs f e , p

≃ₒ-trans :  {𝓤} {𝓥} {𝓦} (α : Ordinal 𝓤) (β : Ordinal 𝓥 ) (γ : Ordinal 𝓦)
          α ≃ₒ β  β ≃ₒ γ  α ≃ₒ γ
≃ₒ-trans α β γ (f , p , e , q) (f' , p' , e' , q') =
  f'  f ,
   x y l  p' (f x) (f y) (p x y l)) ,
  ∘-is-equiv e e' ,
   x y l  q (inverse f' e' x) (inverse f' e' y) (q' x y l))

\end{code}