Martin Escardo, August 2018
The ordinal of ordinals. Based on the HoTT Book, with a few
modifications in some of the definitions and arguments.
This is an example where we are studying sets only, but the
univalence axiom is needed.
\begin{code}
{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
open import UF.Univalence
module Ordinals.OrdinalOfOrdinals
(ua : Univalence)
where
open import MLTT.Spartan
open import Ordinals.Notions
open import Ordinals.Type
open import Ordinals.Underlying
open import Notation.CanonicalMap
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Yoneda
private
fe : FunExt
fe = Univalence-gives-FunExt ua
fe' : Fun-Ext
fe' {𝓤} {𝓥} = fe 𝓤 𝓥
\end{code}
Maps of ordinals. A simulation gives a notion of embedding of
ordinals, making them into a poset, as proved below.
\begin{code}
is-monotone
is-order-embedding
is-initial-segment
is-simulation : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇
is-monotone α β f = (x y : ⟨ α ⟩) → x ≼⟨ α ⟩ y → f x ≼⟨ β ⟩ f y
is-order-embedding α β f = is-order-preserving α β f × is-order-reflecting α β f
is-initial-segment α β f = (x : ⟨ α ⟩) (y : ⟨ β ⟩)
→ y ≺⟨ β ⟩ f x
→ Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y)
is-simulation α β f = is-initial-segment α β f × is-order-preserving α β f
simulations-are-order-preserving : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-order-preserving α β f
simulations-are-order-preserving α β f (i , p) = p
simulations-are-initial-segments : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-initial-segment α β f
simulations-are-initial-segments α β f (i , p) = i
order-equivs-are-simulations : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-order-equiv α β f
→ is-simulation α β f
order-equivs-are-simulations α β f (p , e , q) = h (equivs-are-qinvs f e) q , p
where
h : (d : qinv f)
→ is-order-preserving β α (pr₁ d)
→ is-initial-segment α β f
h (g , ε , η) q x y l = g y , r , η y
where
m : g y ≺⟨ α ⟩ g (f x)
m = q y (f x) l
r : g y ≺⟨ α ⟩ x
r = transport (λ - → g y ≺⟨ α ⟩ -) (ε x) m
order-preservation-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-prop (is-order-preserving α β f)
order-preservation-is-prop {𝓤} {𝓥} α β f =
Π₃-is-prop fe' (λ x y l → Prop-valuedness β (f x) (f y))
order-reflection-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-prop (is-order-reflecting α β f)
order-reflection-is-prop {𝓤} {𝓥} α β f =
Π₃-is-prop fe' (λ x y l → Prop-valuedness α x y)
being-order-embedding-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-prop (is-order-embedding α β f)
being-order-embedding-is-prop α β f = ×-is-prop
(order-preservation-is-prop α β f)
(order-reflection-is-prop α β f)
being-order-equiv-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-prop (is-order-equiv α β f)
being-order-equiv-is-prop α β f = ×-is-prop
(order-preservation-is-prop α β f)
(Σ-is-prop
(being-equiv-is-prop fe f)
(λ e → order-preservation-is-prop β α
(inverse f e)))
simulations-are-lc : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ left-cancellable f
simulations-are-lc α β f (i , p) = γ
where
φ : ∀ x y
→ is-accessible (underlying-order α) x
→ is-accessible (underlying-order α) y
→ f x ＝ f y
→ x ＝ y
φ x y (step s) (step t) r = Extensionality α x y g h
where
g : (u : ⟨ α ⟩) → u ≺⟨ α ⟩ x → u ≺⟨ α ⟩ y
g u l = d
where
a : f u ≺⟨ β ⟩ f y
a = transport (λ - → f u ≺⟨ β ⟩ -) r (p u x l)
b : Σ v ꞉ ⟨ α ⟩ , (v ≺⟨ α ⟩ y) × (f v ＝ f u)
b = i y (f u) a
c : u ＝ pr₁ b
c = φ u (pr₁ b) (s u l) (t (pr₁ b) (pr₁ (pr₂ b))) ((pr₂ (pr₂ b))⁻¹)
d : u ≺⟨ α ⟩ y
d = transport (λ - → - ≺⟨ α ⟩ y) (c ⁻¹) (pr₁ (pr₂ b))
h : (u : ⟨ α ⟩) → u ≺⟨ α ⟩ y → u ≺⟨ α ⟩ x
h u l = d
where
a : f u ≺⟨ β ⟩ f x
a = transport (λ - → f u ≺⟨ β ⟩ -) (r ⁻¹) (p u y l)
b : Σ v ꞉ ⟨ α ⟩ , (v ≺⟨ α ⟩ x) × (f v ＝ f u)
b = i x (f u) a
c : pr₁ b ＝ u
c = φ (pr₁ b) u (s (pr₁ b) (pr₁ (pr₂ b))) (t u l) (pr₂ (pr₂ b))
d : u ≺⟨ α ⟩ x
d = transport (λ - → - ≺⟨ α ⟩ x) c (pr₁ (pr₂ b))
γ : left-cancellable f
γ {x} {y} = φ x y (Well-foundedness α x) (Well-foundedness α y)
being-initial-segment-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-order-preserving α β f
→ is-prop (is-initial-segment α β f)
being-initial-segment-is-prop {𝓤} {𝓥} α β f p = prop-criterion γ
where
γ : is-initial-segment α β f → is-prop (is-initial-segment α β f)
γ i = Π₃-is-prop fe' (λ x z l → φ x z l)
where
φ : ∀ x y → y ≺⟨ β ⟩ f x → is-prop (Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y))
φ x y l (x' , (m , r)) (x'' , (m' , r')) = to-Σ-＝ (a , b)
where
c : f x' ＝ f x''
c = r ∙ r' ⁻¹
j : is-simulation α β f
j = (i , p)
a : x' ＝ x''
a = simulations-are-lc α β f j c
k : is-prop ((x'' ≺⟨ α ⟩ x) × (f x'' ＝ y))
k = ×-is-prop
(Prop-valuedness α x'' x)
(underlying-type-is-set fe β)
b : transport (λ - → (- ≺⟨ α ⟩ x) × (f - ＝ y)) a (m , r) ＝ m' , r'
b = k _ _
\end{code}
The simulations make the ordinals into a poset:
\begin{code}
being-simulation-is-prop : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-prop (is-simulation α β f)
being-simulation-is-prop α β f = ×-prop-criterion
(being-initial-segment-is-prop α β f ,
(λ _ → order-preservation-is-prop α β f))
at-most-one-simulation : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f f' : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-simulation α β f'
→ f ∼ f'
at-most-one-simulation α β f f' (i , p) (i' , p') x = γ
where
φ : ∀ x
→ is-accessible (underlying-order α) x
→ f x ＝ f' x
φ x (step u) = Extensionality β (f x) (f' x) a b
where
IH : ∀ y → y ≺⟨ α ⟩ x → f y ＝ f' y
IH y l = φ y (u y l)
a : (z : ⟨ β ⟩) → z ≺⟨ β ⟩ f x → z ≺⟨ β ⟩ f' x
a z l = transport (λ - → - ≺⟨ β ⟩ f' x) t m
where
s : Σ y ꞉ ⟨ α ⟩ , (y ≺⟨ α ⟩ x) × (f y ＝ z)
s = i x z l
y : ⟨ α ⟩
y = pr₁ s
m : f' y ≺⟨ β ⟩ f' x
m = p' y x (pr₁ (pr₂ s))
t : f' y ＝ z
t = f' y ＝⟨ (IH y (pr₁ (pr₂ s)))⁻¹ ⟩
f y ＝⟨ pr₂ (pr₂ s) ⟩
z ∎
b : (z : ⟨ β ⟩) → z ≺⟨ β ⟩ f' x → z ≺⟨ β ⟩ f x
b z l = transport (λ - → - ≺⟨ β ⟩ f x) t m
where
s : Σ y ꞉ ⟨ α ⟩ , (y ≺⟨ α ⟩ x) × (f' y ＝ z)
s = i' x z l
y : ⟨ α ⟩
y = pr₁ s
m : f y ≺⟨ β ⟩ f x
m = p y x (pr₁ (pr₂ s))
t : f y ＝ z
t = f y ＝⟨ IH y (pr₁ (pr₂ s)) ⟩
f' y ＝⟨ pr₂ (pr₂ s) ⟩
z ∎
γ : f x ＝ f' x
γ = φ x (Well-foundedness α x)
_⊴_ : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇
α ⊴ β = Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-simulation α β f
⊴-is-prop-valued : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → is-prop (α ⊴ β)
⊴-is-prop-valued {𝓤} {𝓥} α β (f , s) (g , t) =
to-subtype-＝ (being-simulation-is-prop α β)
(dfunext fe' (at-most-one-simulation α β f g s t))
⊴-refl : (α : Ordinal 𝓤) → α ⊴ α
⊴-refl α = id ,
(λ x z l → z , l , refl) ,
(λ x y l → l)
⊴-trans : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦)
→ α ⊴ β → β ⊴ γ → α ⊴ γ
⊴-trans α β γ (f , i , p) (g , j , q) = g ∘ f ,
k ,
(λ x y l → q (f x) (f y) (p x y l))
where
k : (x : ⟨ α ⟩) (z : ⟨ γ ⟩) → z ≺⟨ γ ⟩ (g (f x))
→ Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (g (f x') ＝ z)
k x z l = pr₁ b , pr₁ (pr₂ b) , (ap g (pr₂ (pr₂ b)) ∙ pr₂ (pr₂ a))
where
a : Σ y ꞉ ⟨ β ⟩ , (y ≺⟨ β ⟩ f x) × (g y ＝ z)
a = j (f x) z l
y : ⟨ β ⟩
y = pr₁ a
b : Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y)
b = i x y (pr₁ (pr₂ a))
≃ₒ-gives-≃ : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
→ α ≃ₒ β → ⟨ α ⟩ ≃ ⟨ β ⟩
≃ₒ-gives-≃ α β (f , p , e , q) = (f , e)
≃ₒ-is-prop-valued : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
→ is-prop (α ≃ₒ β)
≃ₒ-is-prop-valued α β (f , p , e , q) (f' , p' , e' , q') = γ
where
r : f ∼ f'
r = at-most-one-simulation α β f f'
(order-equivs-are-simulations α β f (p , e , q ))
(order-equivs-are-simulations α β f' (p' , e' , q'))
γ : (f , p , e , q) ＝ (f' , p' , e' , q')
γ = to-subtype-＝
(being-order-equiv-is-prop α β)
(dfunext fe' r)
≃ₒ-to-⊴ : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → α ≃ₒ β → α ⊴ β
≃ₒ-to-⊴ α β (f , e) = (f , order-equivs-are-simulations α β f e)
ordinal-equiv-gives-bisimilarity : (α β : Ordinal 𝓤)
→ α ≃ₒ β
→ (α ⊴ β) × (β ⊴ α)
ordinal-equiv-gives-bisimilarity α β (f , p , e , q) = γ
where
g : ⟨ β ⟩ → ⟨ α ⟩
g = ⌜ f , e ⌝⁻¹
d : is-equiv g
d = ⌜⌝-is-equiv (≃-sym (f , e))
γ : (α ⊴ β) × (β ⊴ α)
γ = (f , order-equivs-are-simulations α β f (p , e , q)) ,
(g , order-equivs-are-simulations β α g (q , d , p))
bisimilarity-gives-ordinal-equiv : (α β : Ordinal 𝓤)
→ α ⊴ β
→ β ⊴ α
→ α ≃ₒ β
bisimilarity-gives-ordinal-equiv α β (f , s) (g , t) = γ
where
ηs : is-simulation β β (f ∘ g)
ηs = pr₂ (⊴-trans β α β (g , t) (f , s))
η : (y : ⟨ β ⟩) → f (g y) ＝ y
η = at-most-one-simulation β β (f ∘ g) id ηs (pr₂ (⊴-refl β))
εs : is-simulation α α (g ∘ f)
εs = pr₂ (⊴-trans α β α (f , s) (g , t))
ε : (x : ⟨ α ⟩) → g (f x) ＝ x
ε = at-most-one-simulation α α (g ∘ f) id εs (pr₂ (⊴-refl α))
γ : α ≃ₒ β
γ = f , pr₂ s , qinvs-are-equivs f (g , ε , η) , pr₂ t
idtoeqₒ : (α β : Ordinal 𝓤) → α ＝ β → α ≃ₒ β
idtoeqₒ α α refl = ≃ₒ-refl α
eqtoidₒ : (α β : Ordinal 𝓤) → α ≃ₒ β → α ＝ β
eqtoidₒ {𝓤} α β (f , p , e , q) = γ
where
A : (Y : 𝓤 ̇ ) → ⟨ α ⟩ ≃ Y → 𝓤 ⁺ ̇
A Y e = (σ : OrdinalStructure Y)
→ is-order-preserving α (Y , σ) ⌜ e ⌝
→ is-order-preserving (Y , σ) α ⌜ e ⌝⁻¹
→ α ＝ (Y , σ)
a : A ⟨ α ⟩ (≃-refl ⟨ α ⟩)
a σ φ ψ = g
where
b : (x x' : ⟨ α ⟩) → (x ≺⟨ α ⟩ x') ＝ (x ≺⟨ ⟨ α ⟩ , σ ⟩ x')
b x x' = univalence-gives-propext (ua 𝓤)
(Prop-valuedness α x x')
(Prop-valuedness (⟨ α ⟩ , σ) x x')
(φ x x')
(ψ x x')
c : underlying-order α ＝ underlying-order (⟨ α ⟩ , σ)
c = dfunext fe' (λ x → dfunext fe' (b x))
d : structure α ＝ σ
d = pr₁-lc (λ {_<_} → being-well-order-is-prop _<_ fe) c
g : α ＝ (⟨ α ⟩ , σ)
g = to-Σ-＝' d
γ : α ＝ β
γ = JEq (ua 𝓤) ⟨ α ⟩ A a ⟨ β ⟩ (f , e) (structure β) p q
UAₒ : (α β : Ordinal 𝓤) → is-equiv (idtoeqₒ α β)
UAₒ {𝓤} α = nats-with-sections-are-equivs α
(idtoeqₒ α)
(λ β → eqtoidₒ α β , η β)
where
η : (β : Ordinal 𝓤) (e : α ≃ₒ β)
→ idtoeqₒ α β (eqtoidₒ α β e) ＝ e
η β e = ≃ₒ-is-prop-valued α β (idtoeqₒ α β (eqtoidₒ α β e)) e
the-type-of-ordinals-is-a-set : is-set (Ordinal 𝓤)
the-type-of-ordinals-is-a-set {𝓤} {α} {β} = equiv-to-prop
(idtoeqₒ α β , UAₒ α β)
(≃ₒ-is-prop-valued α β)
UAₒ-≃ : (α β : Ordinal 𝓤) → (α ＝ β) ≃ (α ≃ₒ β)
UAₒ-≃ α β = idtoeqₒ α β , UAₒ α β
the-type-of-ordinals-is-locally-small : is-locally-small (Ordinal 𝓤)
the-type-of-ordinals-is-locally-small α β = (α ≃ₒ β) , ≃-sym (UAₒ-≃ α β)
\end{code}
One of the many applications of the univalence axiom is to manufacture
examples of types which are not sets. Here we have instead used it to
prove that a certain type is a set.
A corollary of the above is that the ordinal order _⊴_ is
antisymmetric.
\begin{code}
⊴-antisym : (α β : Ordinal 𝓤)
→ α ⊴ β
→ β ⊴ α
→ α ＝ β
⊴-antisym α β l m = eqtoidₒ α β (bisimilarity-gives-ordinal-equiv α β l m)
\end{code}
Any lower set α ↓ a of a point a : ⟨ α ⟩ forms a (sub-)ordinal:
\begin{code}
_↓_ : (α : Ordinal 𝓤) → ⟨ α ⟩ → Ordinal 𝓤
α ↓ a = (Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a) , _<_ , p , w , e , t
where
_<_ : (Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a) → (Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a) → _ ̇
(y , _) < (z , _) = y ≺⟨ α ⟩ z
p : is-prop-valued _<_
p (x , _) (y , _) = Prop-valuedness α x y
w : is-well-founded _<_
w (x , l) = f x (Well-foundedness α x) l
where
f : ∀ x → is-accessible (underlying-order α) x → ∀ l → is-accessible _<_ (x , l)
f x (step s) l = step (λ σ m → f (pr₁ σ) (s (pr₁ σ) m) (pr₂ σ))
e : is-extensional _<_
e (x , l) (y , m) f g =
to-subtype-＝
(λ z → Prop-valuedness α z a)
(Extensionality α x y
(λ u n → f (u , Transitivity α u x a n l) n)
(λ u n → g (u , Transitivity α u y a n m) n))
t : is-transitive _<_
t (x , _) (y , _) (z , _) = Transitivity α x y z
segment-inclusion : (α : Ordinal 𝓤) (a : ⟨ α ⟩)
→ ⟨ α ↓ a ⟩ → ⟨ α ⟩
segment-inclusion α a = pr₁
segment-inclusion-bound : (α : Ordinal 𝓤) (a : ⟨ α ⟩)
→ (x : ⟨ α ↓ a ⟩) → segment-inclusion α a x ≺⟨ α ⟩ a
segment-inclusion-bound α a = pr₂
segment-inclusion-is-simulation : (α : Ordinal 𝓤) (a : ⟨ α ⟩)
→ is-simulation (α ↓ a) α (segment-inclusion α a)
segment-inclusion-is-simulation α a = i , p
where
i : is-initial-segment (α ↓ a) α (segment-inclusion α a)
i (x , l) y m = (y , Transitivity α y x a m l) , m , refl
p : is-order-preserving (α ↓ a) α (segment-inclusion α a)
p x x' = id
segment-⊴ : (α : Ordinal 𝓤) (a : ⟨ α ⟩)
→ (α ↓ a) ⊴ α
segment-⊴ α a = segment-inclusion α a , segment-inclusion-is-simulation α a
↓-⊴-lc : (α : Ordinal 𝓤) (a b : ⟨ α ⟩)
→ (α ↓ a) ⊴ (α ↓ b ) → a ≼⟨ α ⟩ b
↓-⊴-lc {𝓤} α a b (f , s) u l = n
where
h : segment-inclusion α a ∼ segment-inclusion α b ∘ f
h = at-most-one-simulation (α ↓ a) α
(segment-inclusion α a)
(segment-inclusion α b ∘ f)
(segment-inclusion-is-simulation α a)
(pr₂ (⊴-trans (α ↓ a) (α ↓ b) α
(f , s)
(segment-⊴ α b)))
v : ⟨ α ⟩
v = segment-inclusion α b (f (u , l))
m : v ≺⟨ α ⟩ b
m = segment-inclusion-bound α b (f (u , l))
q : u ＝ v
q = h (u , l)
n : u ≺⟨ α ⟩ b
n = transport⁻¹ (λ - → - ≺⟨ α ⟩ b) q m
↓-lc : (α : Ordinal 𝓤) (a b : ⟨ α ⟩)
→ α ↓ a ＝ α ↓ b → a ＝ b
↓-lc α a b p =
Extensionality α a b
(↓-⊴-lc α a b (transport (λ - → (α ↓ a) ⊴ -) p (⊴-refl (α ↓ a))))
(↓-⊴-lc α b a (transport⁻¹ (λ - → (α ↓ b) ⊴ -) p (⊴-refl (α ↓ b))))
\end{code}
We are now ready to make the type of ordinals into an ordinal.
\begin{code}
_⊲_ : Ordinal 𝓤 → Ordinal 𝓤 → 𝓤 ⁺ ̇
α ⊲ β = Σ b ꞉ ⟨ β ⟩ , α ＝ (β ↓ b)
⊲-is-prop-valued : (α β : Ordinal 𝓤) → is-prop (α ⊲ β)
⊲-is-prop-valued {𝓤} α β (b , p) (b' , p') = γ
where
q = (β ↓ b) ＝⟨ p ⁻¹ ⟩
α ＝⟨ p' ⟩
(β ↓ b') ∎
r : b ＝ b'
r = ↓-lc β b b' q
γ : (b , p) ＝ (b' , p')
γ = to-subtype-＝ (λ x → the-type-of-ordinals-is-a-set) r
\end{code}
NB. We could instead define α ⊲ β to mean that we have b with
α ≃ₒ (β ↓ b), or with α ⊴ (β ↓ b) and (β ↓ b) ⊴ α, by antisymmetry,
and these two alternative, equivalent, definitions make ⊲ to have
values in the universe 𝓤 rather than the next universe 𝓤 ⁺.
Added 23 December 2020. The previous observation turns out to be
useful to resize down the relation _⊲_ in certain applications. So we
make it official:
\begin{code}
_⊲⁻_ : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇
α ⊲⁻ β = Σ b ꞉ ⟨ β ⟩ , α ≃ₒ (β ↓ b)
⊲-is-equivalent-to-⊲⁻ : (α β : Ordinal 𝓤) → (α ⊲ β) ≃ (α ⊲⁻ β)
⊲-is-equivalent-to-⊲⁻ α β = Σ-cong (λ (b : ⟨ β ⟩) → UAₒ-≃ α (β ↓ b))
\end{code}
Back to the past.
A lower set of a lower set is a lower set:
\begin{code}
iterated-↓ : (α : Ordinal 𝓤) (a b : ⟨ α ⟩) (l : b ≺⟨ α ⟩ a)
→ ((α ↓ a ) ↓ (b , l)) ＝ (α ↓ b)
iterated-↓ α a b l = ⊴-antisym ((α ↓ a) ↓ (b , l)) (α ↓ b)
(φ α a b l) (ψ α a b l)
where
φ : (α : Ordinal 𝓤) (b u : ⟨ α ⟩) (l : u ≺⟨ α ⟩ b)
→ ((α ↓ b ) ↓ (u , l)) ⊴ (α ↓ u)
φ α b u l = f , i , p
where
f : ⟨ (α ↓ b) ↓ (u , l) ⟩ → ⟨ α ↓ u ⟩
f ((x , m) , n) = x , n
i : (w : ⟨ (α ↓ b) ↓ (u , l) ⟩) (t : ⟨ α ↓ u ⟩)
→ t ≺⟨ α ↓ u ⟩ f w
→ Σ w' ꞉ ⟨ (α ↓ b) ↓ (u , l) ⟩ , (w' ≺⟨ (α ↓ b) ↓ (u , l) ⟩ w) × (f w' ＝ t)
i ((x , m) , n) (x' , m') n' = ((x' , Transitivity α x' u b m' l) , m') ,
(n' , refl)
p : (w w' : ⟨ (α ↓ b) ↓ (u , l) ⟩)
→ w ≺⟨ (α ↓ b) ↓ (u , l) ⟩ w' → f w ≺⟨ α ↓ u ⟩ (f w')
p w w' = id
ψ : (α : Ordinal 𝓤) (b u : ⟨ α ⟩) (l : u ≺⟨ α ⟩ b)
→ (α ↓ u) ⊴ ((α ↓ b ) ↓ (u , l))
ψ α b u l = f , (i , p)
where
f : ⟨ α ↓ u ⟩ → ⟨ (α ↓ b) ↓ (u , l) ⟩
f (x , n) = ((x , Transitivity α x u b n l) , n)
i : (t : ⟨ α ↓ u ⟩)
(w : ⟨ (α ↓ b) ↓ (u , l) ⟩)
→ w ≺⟨ (α ↓ b) ↓ (u , l) ⟩ f t
→ Σ t' ꞉ ⟨ α ↓ u ⟩ , (t' ≺⟨ α ↓ u ⟩ t) × (f t' ＝ w)
i (x , n) ((x' , m') , n') o = (x' , n') , (o , r)
where
r : ((x' , Transitivity α x' u b n' l) , n') ＝ (x' , m') , n'
r = ap (λ - → ((x' , -) , n'))
(Prop-valuedness α x' b (Transitivity α x' u b n' l) m')
p : (t t' : ⟨ α ↓ u ⟩) → t ≺⟨ α ↓ u ⟩ t' → f t ≺⟨ (α ↓ b) ↓ (u , l) ⟩ f t'
p t t' = id
\end{code}
Therefore the map (α ↓ -) reflects and preserves order:
\begin{code}
↓-reflects-order : (α : Ordinal 𝓤) (a b : ⟨ α ⟩)
→ (α ↓ a) ⊲ (α ↓ b)
→ a ≺⟨ α ⟩ b
↓-reflects-order α a b ((u , l) , p) = γ
where
have : type-of l ＝ (u ≺⟨ α ⟩ b)
have = refl
q : (α ↓ a) ＝ (α ↓ u)
q = (α ↓ a) ＝⟨ p ⟩
((α ↓ b) ↓ (u , l)) ＝⟨ iterated-↓ α b u l ⟩
(α ↓ u) ∎
r : a ＝ u
r = ↓-lc α a u q
γ : a ≺⟨ α ⟩ b
γ = transport⁻¹ (λ - → - ≺⟨ α ⟩ b) r l
↓-preserves-order : (α : Ordinal 𝓤) (a b : ⟨ α ⟩)
→ a ≺⟨ α ⟩ b
→ (α ↓ a) ⊲ (α ↓ b)
↓-preserves-order α a b l = (a , l) , ((iterated-↓ α b a l)⁻¹)
\end{code}
It remains to show that _⊲_ is a well-order:
\begin{code}
↓-accessible : (α : Ordinal 𝓤) (a : ⟨ α ⟩)
→ is-accessible _⊲_ (α ↓ a)
↓-accessible {𝓤} α a = f a (Well-foundedness α a)
where
f : (a : ⟨ α ⟩)
→ is-accessible (underlying-order α) a
→ is-accessible _⊲_ (α ↓ a)
f a (step s) = step g
where
IH : (b : ⟨ α ⟩) → b ≺⟨ α ⟩ a → is-accessible _⊲_ (α ↓ b)
IH b l = f b (s b l)
g : (β : Ordinal 𝓤) → β ⊲ (α ↓ a) → is-accessible _⊲_ β
g β ((b , l) , p) = transport⁻¹ (is-accessible _⊲_) q (IH b l)
where
q : β ＝ (α ↓ b)
q = p ∙ iterated-↓ α a b l
⊲-is-well-founded : is-well-founded (_⊲_ {𝓤})
⊲-is-well-founded {𝓤} α = step g
where
g : (β : Ordinal 𝓤) → β ⊲ α → is-accessible _⊲_ β
g β (b , p) = transport⁻¹ (is-accessible _⊲_) p (↓-accessible α b)
⊲-is-extensional : is-extensional (_⊲_ {𝓤})
⊲-is-extensional α β f g = ⊴-antisym α β
((λ x → pr₁ (φ x)) , i , p)
((λ y → pr₁ (γ y)) , j , q)
where
φ : (x : ⟨ α ⟩) → Σ y ꞉ ⟨ β ⟩ , α ↓ x ＝ β ↓ y
φ x = f (α ↓ x) (x , refl)
γ : (y : ⟨ β ⟩) → Σ x ꞉ ⟨ α ⟩ , β ↓ y ＝ α ↓ x
γ y = g (β ↓ y) (y , refl)
η : (x : ⟨ α ⟩) → pr₁ (γ (pr₁ (φ x))) ＝ x
η x = (↓-lc α x (pr₁ (γ (pr₁ (φ x)))) a)⁻¹
where
a : (α ↓ x) ＝ (α ↓ pr₁ (γ (pr₁ (φ x))))
a = pr₂ (φ x) ∙ pr₂ (γ (pr₁ (φ x)))
ε : (y : ⟨ β ⟩) → pr₁ (φ (pr₁ (γ y))) ＝ y
ε y = (↓-lc β y (pr₁ (φ (pr₁ (γ y)))) a)⁻¹
where
a : (β ↓ y) ＝ (β ↓ pr₁ (φ (pr₁ (γ y))))
a = pr₂ (γ y) ∙ pr₂ (φ (pr₁ (γ y)))
p : is-order-preserving α β (λ x → pr₁ (φ x))
p x x' l = ↓-reflects-order β (pr₁ (φ x)) (pr₁ (φ x')) b
where
a : (α ↓ x) ⊲ (α ↓ x')
a = ↓-preserves-order α x x' l
b : (β ↓ pr₁ (φ x)) ⊲ (β ↓ pr₁ (φ x'))
b = transport₂ _⊲_ (pr₂ (φ x)) (pr₂ (φ x')) a
q : is-order-preserving β α (λ y → pr₁ (γ y))
q y y' l = ↓-reflects-order α (pr₁ (γ y)) (pr₁ (γ y')) b
where
a : (β ↓ y) ⊲ (β ↓ y')
a = ↓-preserves-order β y y' l
b : (α ↓ pr₁ (γ y)) ⊲ (α ↓ pr₁ (γ y'))
b = transport₂ _⊲_ (pr₂ (γ y)) (pr₂ (γ y')) a
i : is-initial-segment α β (λ x → pr₁ (φ x))
i x y l = pr₁ (γ y) , transport (λ - → pr₁ (γ y) ≺⟨ α ⟩ -) (η x) a , ε y
where
a : pr₁ (γ y) ≺⟨ α ⟩ (pr₁ (γ (pr₁ (φ x))))
a = q y (pr₁ (φ x)) l
j : is-initial-segment β α (λ y → pr₁ (γ y))
j y x l = pr₁ (φ x) , transport (λ - → pr₁ (φ x) ≺⟨ β ⟩ -) (ε y) a , η x
where
a : pr₁ (φ x) ≺⟨ β ⟩ (pr₁ (φ (pr₁ (γ y))))
a = p x (pr₁ (γ y)) l
⊲-is-transitive : is-transitive (_⊲_ {𝓤})
⊲-is-transitive {𝓤} α β φ (a , p) (b , q) = γ
where
t : (q : β ＝ (φ ↓ b)) → (β ↓ a) ＝ ((φ ↓ b) ↓ transport ⟨_⟩ q a)
t refl = refl
u : ⟨ φ ↓ b ⟩
u = transport (⟨_⟩) q a
c : ⟨ φ ⟩
c = pr₁ u
l : c ≺⟨ φ ⟩ b
l = pr₂ u
r : α ＝ (φ ↓ c)
r = α ＝⟨ p ⟩
(β ↓ a) ＝⟨ t q ⟩
((φ ↓ b) ↓ u) ＝⟨ iterated-↓ φ b c l ⟩
(φ ↓ c) ∎
γ : Σ c ꞉ ⟨ φ ⟩ , α ＝ (φ ↓ c)
γ = c , r
⊲-is-well-order : is-well-order (_⊲_ {𝓤})
⊲-is-well-order = ⊲-is-prop-valued ,
⊲-is-well-founded ,
⊲-is-extensional ,
⊲-is-transitive
\end{code}
We denote the ordinal of ordinals in the universe 𝓤 by OO 𝓤. It lives
in the next universe 𝓤 ⁺.
\begin{code}
OO : (𝓤 : Universe) → Ordinal (𝓤 ⁺)
OO 𝓤 = Ordinal 𝓤 , _⊲_ , ⊲-is-well-order
\end{code}
Any ordinal in OO 𝓤 is embedded in OO 𝓤 as an initial segment:
\begin{code}
ordinals-in-OO-are-embedded-in-OO : (α : ⟨ OO 𝓤 ⟩) → α ⊴ OO 𝓤
ordinals-in-OO-are-embedded-in-OO {𝓤} α = (λ x → α ↓ x) , i , ↓-preserves-order α
where
i : is-initial-segment α (OO 𝓤) (λ x → α ↓ x)
i x β ((u , l) , p) = u , l , ((p ∙ iterated-↓ α x u l)⁻¹)
\end{code}
Any ordinal in OO 𝓤 is a lower set of OO 𝓤:
\begin{code}
ordinals-in-OO-are-lowersets-of-OO : (α : ⟨ OO 𝓤 ⟩) → α ≃ₒ (OO 𝓤 ↓ α)
ordinals-in-OO-are-lowersets-of-OO {𝓤} α = f , p , ((g , η) , (g , ε)) , q
where
f : ⟨ α ⟩ → ⟨ OO 𝓤 ↓ α ⟩
f x = α ↓ x , x , refl
p : is-order-preserving α (OO 𝓤 ↓ α) f
p x y l = (x , l) , ((iterated-↓ α y x l)⁻¹)
g : ⟨ OO 𝓤 ↓ α ⟩ → ⟨ α ⟩
g (β , x , r) = x
η : (σ : ⟨ OO 𝓤 ↓ α ⟩) → f (g σ) ＝ σ
η (.(α ↓ x) , x , refl) = refl
ε : (x : ⟨ α ⟩) → g (f x) ＝ x
ε x = refl
q : is-order-preserving (OO 𝓤 ↓ α) α g
q (.(α ↓ x) , x , refl) (.(α ↓ x') , x' , refl) = ↓-reflects-order α x x'
\end{code}
Here are some additional observations about the various maps of
ordinals:
\begin{code}
lc-initial-segments-are-order-reflecting : (α β : Ordinal 𝓤)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-initial-segment α β f
→ left-cancellable f
→ is-order-reflecting α β f
lc-initial-segments-are-order-reflecting α β f i c x y l = m
where
a : Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ y) × (f x' ＝ f x)
a = i y (f x) l
m : x ≺⟨ α ⟩ y
m = transport (λ - → - ≺⟨ α ⟩ y) (c (pr₂ (pr₂ a))) (pr₁ (pr₂ a))
simulations-are-order-reflecting : (α β : Ordinal 𝓤)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-order-reflecting α β f
simulations-are-order-reflecting α β f (i , p) =
lc-initial-segments-are-order-reflecting α β f i
(simulations-are-lc α β f (i , p))
order-embeddings-are-lc : (α β : Ordinal 𝓤) (f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-order-embedding α β f
→ left-cancellable f
order-embeddings-are-lc α β f (p , r) {x} {y} s = γ
where
a : (u : ⟨ α ⟩) → u ≺⟨ α ⟩ x → u ≺⟨ α ⟩ y
a u l = r u y j
where
i : f u ≺⟨ β ⟩ f x
i = p u x l
j : f u ≺⟨ β ⟩ f y
j = transport (λ - → f u ≺⟨ β ⟩ -) s i
b : (u : ⟨ α ⟩) → u ≺⟨ α ⟩ y → u ≺⟨ α ⟩ x
b u l = r u x j
where
i : f u ≺⟨ β ⟩ f y
i = p u y l
j : f u ≺⟨ β ⟩ f x
j = transport⁻¹ (λ - → f u ≺⟨ β ⟩ -) s i
γ : x ＝ y
γ = Extensionality α x y a b
order-embedings-are-embeddings : (α β : Ordinal 𝓤) (f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-order-embedding α β f
→ is-embedding f
order-embedings-are-embeddings α β f (p , r) =
lc-maps-into-sets-are-embeddings f
(order-embeddings-are-lc α β f (p , r))
(underlying-type-is-set fe β)
simulations-are-monotone : (α β : Ordinal 𝓤)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-monotone α β f
simulations-are-monotone α β f (i , p) = φ
where
φ : (x y : ⟨ α ⟩)
→ ((z : ⟨ α ⟩) → z ≺⟨ α ⟩ x → z ≺⟨ α ⟩ y)
→ (t : ⟨ β ⟩) → t ≺⟨ β ⟩ f x → t ≺⟨ β ⟩ f y
φ x y ψ t l = transport (λ - → - ≺⟨ β ⟩ f y) b d
where
z : ⟨ α ⟩
z = pr₁ (i x t l)
a : z ≺⟨ α ⟩ x
a = pr₁ (pr₂ (i x t l))
b : f z ＝ t
b = pr₂ (pr₂ (i x t l))
c : z ≺⟨ α ⟩ y
c = ψ z a
d : f z ≺⟨ β ⟩ f y
d = p z y c
\end{code}
Example. Classically, the ordinals ω +ₒ 𝟙ₒ and ℕ∞ₒ are equal.
Constructively, we have (ω +ₒ 𝟙ₒ) ⊴ ℕ∞ₒ, but the inequality in the
other direction is equivalent to LPO.
\begin{code}
module ℕ∞-in-Ord where
open import Taboos.LPO fe
open import Naturals.Order
open import Ordinals.Arithmetic fe
open import CoNaturals.GenericConvergentSequence
fact : (ω +ₒ 𝟙ₒ) ⊴ ℕ∞ₒ
fact = ι𝟙 , i , p
where
i : (x : ⟨ ω +ₒ 𝟙ₒ ⟩) (y : ⟨ ℕ∞ₒ ⟩)
→ y ≺⟨ ℕ∞ₒ ⟩ ι𝟙 x
→ Σ x' ꞉ ⟨ ω +ₒ 𝟙ₒ ⟩ , (x' ≺⟨ ω +ₒ 𝟙ₒ ⟩ x) × (ι𝟙 x' ＝ y)
i (inl m) y (n , r , l) = inl n , ⊏-gives-< n m l , (r ⁻¹)
i (inr *) y (n , r , l) = inl n , * , (r ⁻¹)
p : (x y : ⟨ ω +ₒ 𝟙ₒ ⟩)
→ x ≺⟨ ω +ₒ 𝟙ₒ ⟩ y
→ ι𝟙 x ≺⟨ ℕ∞ₒ ⟩ ι𝟙 y
p (inl n) (inl m) l = ℕ-to-ℕ∞-order-preserving n m l
p (inl n) (inr *) * = ∞-≺-largest n
p (inr *) (inl m) l = 𝟘-elim l
p (inr *) (inr *) l = 𝟘-elim l
converse-fails-constructively : ℕ∞ₒ ⊴ (ω +ₒ 𝟙ₒ) → LPO
converse-fails-constructively l = γ
where
b : (ω +ₒ 𝟙ₒ) ≃ₒ ℕ∞ₒ
b = bisimilarity-gives-ordinal-equiv (ω +ₒ 𝟙ₒ) ℕ∞ₒ fact l
e : is-equiv ι𝟙
e = pr₂ (≃ₒ-gives-≃ (ω +ₒ 𝟙ₒ) ℕ∞ₒ b)
γ : LPO
γ = ι𝟙-has-section-gives-LPO (equivs-have-sections ι𝟙 e)
converse-fails-constructively-converse : LPO → ℕ∞ₒ ⊴ (ω +ₒ 𝟙ₒ)
converse-fails-constructively-converse lpo = (λ x → ι𝟙-inverse x (lpo x)) ,
(λ x → i x (lpo x)) ,
(λ x y → p x y (lpo x) (lpo y))
where
ι𝟙-inverse-inl : (u : ℕ∞) (d : decidable (Σ n ꞉ ℕ , u ＝ ι n))
→ (m : ℕ) → u ＝ ι m → ι𝟙-inverse u d ＝ inl m
ι𝟙-inverse-inl . (ι n) (inl (n , refl)) m q = ap inl (ℕ-to-ℕ∞-lc q)
ι𝟙-inverse-inl u (inr g) m q = 𝟘-elim (g (m , q))
i : (x : ℕ∞) (d : decidable (Σ n ꞉ ℕ , x ＝ ι n)) (y : ℕ + 𝟙)
→ y ≺⟨ ω +ₒ 𝟙ₒ ⟩ ι𝟙-inverse x d
→ Σ x' ꞉ ℕ∞ , (x' ≺⟨ ℕ∞ₒ ⟩ x) × (ι𝟙-inverse x' (lpo x') ＝ y)
i .(ι n) (inl (n , refl)) (inl m) l =
ι m ,
ℕ-to-ℕ∞-order-preserving m n l ,
ι𝟙-inverse-inl (ι m) (lpo (ι m)) m refl
i .(ι n) (inl (n , refl)) (inr *) l = 𝟘-elim l
i x (inr g) (inl n) * =
ι n ,
transport (underlying-order ℕ∞ₒ (ι n))
((not-finite-is-∞ (fe 𝓤₀ 𝓤₀) (curry g)) ⁻¹)
(∞-≺-largest n) ,
ι𝟙-inverse-inl (ι n) (lpo (ι n)) n refl
i x (inr g) (inr *) l = 𝟘-elim l
p : (x y : ℕ∞) (d : decidable (Σ n ꞉ ℕ , x ＝ ι n)) (e : decidable (Σ m ꞉ ℕ , y ＝ ι m))
→ x ≺⟨ ℕ∞ₒ ⟩ y
→ ι𝟙-inverse x d ≺⟨ ω +ₒ 𝟙ₒ ⟩ ι𝟙-inverse y e
p .(ι n) .(ι m) (inl (n , refl)) (inl (m , refl)) (k , r , l) =
transport⁻¹ (λ - → - <ℕ m) (ℕ-to-ℕ∞-lc r) (⊏-gives-< k m l)
p .(ι n) y (inl (n , refl)) (inr f) l = ⋆
p x y (inr f) e (k , r , l) =
𝟘-elim (∞-is-not-finite k ((not-finite-is-∞ (fe 𝓤₀ 𝓤₀) (curry f))⁻¹ ∙ r))
corollary₁ : LPO → ℕ∞ₒ ≃ₒ (ω +ₒ 𝟙ₒ)
corollary₁ lpo = bisimilarity-gives-ordinal-equiv
ℕ∞ₒ (ω +ₒ 𝟙ₒ)
(converse-fails-constructively-converse lpo) fact
corollary₂ : LPO → ℕ∞ ≃ (ℕ + 𝟙)
corollary₂ lpo = ≃ₒ-gives-≃ ℕ∞ₒ (ω +ₒ 𝟙ₒ) (corollary₁ lpo)
corollary₃ : LPO → ℕ∞ₒ ＝ (ω +ₒ 𝟙ₒ)
corollary₃ lpo = eqtoidₒ ℕ∞ₒ (ω +ₒ 𝟙ₒ) (corollary₁ lpo)
corollary₄ : LPO → ℕ∞ ＝ (ℕ + 𝟙)
corollary₄ lpo = eqtoid (ua 𝓤₀) ℕ∞ (ℕ + 𝟙) (corollary₂ lpo)
\end{code}
Added 19-20 January 2021.
The partial order _⊴_ is equivalent to _≼_.
We first observe that, almost tautologically, the relation α ≼ β is
logically equivalent to the condition (a : ⟨ α ⟩) → (α ↓ a) ⊲ β.
\begin{code}
_≼_ _≾_ : Ordinal 𝓤 → Ordinal 𝓤 → 𝓤 ⁺ ̇
α ≼ β = α ≼⟨ OO _ ⟩ β
α ≾ β = ¬ (β ≼ α)
to-≼ : {α β : Ordinal 𝓤}
→ ((a : ⟨ α ⟩) → (α ↓ a) ⊲ β)
→ α ≼ β
to-≼ {𝓤} {α} {β} ϕ α' (a , p) = m
where
l : (α ↓ a) ⊲ β
l = ϕ a
m : α' ⊲ β
m = transport (_⊲ β) (p ⁻¹) l
from-≼ : {α β : Ordinal 𝓤}
→ α ≼ β
→ (a : ⟨ α ⟩) → (α ↓ a) ⊲ β
from-≼ {𝓤} {α} {β} l a = l (α ↓ a) m
where
m : (α ↓ a) ⊲ α
m = (a , refl)
⊴-gives-≼ : (α β : Ordinal 𝓤) → α ⊴ β → α ≼ β
⊴-gives-≼ α β (f , f-is-initial-segment , f-is-order-preserving) α' (a , p) = l
where
f-is-simulation : is-simulation α β f
f-is-simulation = f-is-initial-segment , f-is-order-preserving
g : ⟨ α ↓ a ⟩ → ⟨ β ↓ f a ⟩
g (x , l) = f x , f-is-order-preserving x a l
h : ⟨ β ↓ f a ⟩ → ⟨ α ↓ a ⟩
h (y , m) = pr₁ σ , pr₁ (pr₂ σ)
where
σ : Σ x ꞉ ⟨ α ⟩ , (x ≺⟨ α ⟩ a) × (f x ＝ y)
σ = f-is-initial-segment a y m
η : h ∘ g ∼ id
η (x , l) = to-subtype-＝ (λ - → Prop-valuedness α - a) r
where
σ : Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ a) × (f x' ＝ f x)
σ = f-is-initial-segment a (f x) (f-is-order-preserving x a l)
x' = pr₁ σ
have : pr₁ (h (g (x , l))) ＝ x'
have = refl
s : f x' ＝ f x
s = pr₂ (pr₂ σ)
r : x' ＝ x
r = simulations-are-lc α β f f-is-simulation s
ε : g ∘ h ∼ id
ε (y , m) = to-subtype-＝ (λ - → Prop-valuedness β - (f a)) r
where
r : f (pr₁ (f-is-initial-segment a y m)) ＝ y
r = pr₂ (pr₂ (f-is-initial-segment a y m))
g-is-order-preserving : is-order-preserving (α ↓ a) (β ↓ f a) g
g-is-order-preserving (x , _) (x' , _) = f-is-order-preserving x x'
h-is-order-preserving : is-order-preserving (β ↓ f a) (α ↓ a) h
h-is-order-preserving (y , m) (y' , m') l = o
where
have : y ≺⟨ β ⟩ y'
have = l
σ = f-is-initial-segment a y m
σ' = f-is-initial-segment a y' m'
x = pr₁ σ
x' = pr₁ σ'
s : f x ＝ y
s = pr₂ (pr₂ σ)
s' : f x' ＝ y'
s' = pr₂ (pr₂ σ')
t : f x ≺⟨ β ⟩ f x'
t = transport₂ (λ y y' → y ≺⟨ β ⟩ y') (s ⁻¹) (s' ⁻¹) l
o : x ≺⟨ α ⟩ x'
o = simulations-are-order-reflecting α β f f-is-simulation x x' t
q : (α ↓ a) ＝ (β ↓ f a)
q = eqtoidₒ (α ↓ a) (β ↓ f a)
(g ,
g-is-order-preserving ,
qinvs-are-equivs g (h , η , ε) ,
h-is-order-preserving)
l : α' ⊲ β
l = transport (_⊲ β) (p ⁻¹) (f a , q)
\end{code}
For the converse of the above, it suffices to show the following:
\begin{code}
to-⊴ : (α β : Ordinal 𝓤)
→ ((a : ⟨ α ⟩) → (α ↓ a) ⊲ β)
→ α ⊴ β
to-⊴ α β ϕ = g
where
f : ⟨ α ⟩ → ⟨ β ⟩
f a = pr₁ (ϕ a)
f-property : (a : ⟨ α ⟩) → (α ↓ a) ＝ (β ↓ f a)
f-property a = pr₂ (ϕ a)
f-is-order-preserving : is-order-preserving α β f
f-is-order-preserving a a' l = o
where
m : (α ↓ a) ⊲ (α ↓ a')
m = ↓-preserves-order α a a' l
n : (β ↓ f a) ⊲ (β ↓ f a')
n = transport₂ _⊲_ (f-property a) (f-property a') m
o : f a ≺⟨ β ⟩ f a'
o = ↓-reflects-order β (f a) (f a') n
f-is-initial-segment : (x : ⟨ α ⟩) (y : ⟨ β ⟩)
→ y ≺⟨ β ⟩ f x
→ Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y)
f-is-initial-segment x y l = x' , o , (q ⁻¹)
where
m : (β ↓ y) ⊲ (β ↓ f x)
m = ↓-preserves-order β y (f x) l
n : (β ↓ y) ⊲ (α ↓ x)
n = transport ((β ↓ y) ⊲_) ((f-property x)⁻¹) m
x' : ⟨ α ⟩
x' = pr₁ (pr₁ n)
o : x' ≺⟨ α ⟩ x
o = pr₂ (pr₁ n)
p = (β ↓ y) ＝⟨ pr₂ n ⟩
((α ↓ x) ↓ (x' , o)) ＝⟨ iterated-↓ α x x' o ⟩
(α ↓ x') ＝⟨ f-property x' ⟩
(β ↓ f x') ∎
q : y ＝ f x'
q = ↓-lc β y (f x') p
g : α ⊴ β
g = f , f-is-initial-segment , f-is-order-preserving
≼-gives-⊴ : (α β : Ordinal 𝓤) → α ≼ β → α ⊴ β
≼-gives-⊴ {𝓤} α β l = to-⊴ α β (from-≼ l)
⊲-gives-≼ : (α β : Ordinal 𝓤) → α ⊲ β → α ≼ β
⊲-gives-≼ {𝓤} α β l α' m = Transitivity (OO 𝓤) α' α β m l
⊲-gives-⊴ : (α β : Ordinal 𝓤) → α ⊲ β → α ⊴ β
⊲-gives-⊴ α β l = ≼-gives-⊴ α β (⊲-gives-≼ α β l)
\end{code}
Added 7 November 2022 by Tom de Jong.
A consequence of the above constructions is that a simulation preserves initial
segments in the following sense:
\begin{code}
simulations-preserve-↓ : (α β : Ordinal 𝓤) ((f , _) : α ⊴ β)
→ ((a : ⟨ α ⟩) → α ↓ a ＝ β ↓ f a)
simulations-preserve-↓ α β 𝕗 a = pr₂ (from-≼ (⊴-gives-≼ α β 𝕗) a)
\end{code}
End of addition.
Transfinite induction on the ordinal of ordinals:
\begin{code}
transfinite-induction-on-OO : (P : Ordinal 𝓤 → 𝓥 ̇ )
→ ((α : Ordinal 𝓤) → ((a : ⟨ α ⟩) → P (α ↓ a)) → P α)
→ (α : Ordinal 𝓤) → P α
transfinite-induction-on-OO {𝓤} {𝓥} P f = Transfinite-induction (OO 𝓤) P f'
where
f' : (α : Ordinal 𝓤)
→ ((α' : Ordinal 𝓤) → α' ⊲ α → P α')
→ P α
f' α g = f α (λ a → g (α ↓ a) (a , refl))
transfinite-recursion-on-OO : (X : 𝓥 ̇ )
→ ((α : Ordinal 𝓤) → (⟨ α ⟩ → X) → X)
→ Ordinal 𝓤 → X
transfinite-recursion-on-OO {𝓤} {𝓥} X = transfinite-induction-on-OO (λ _ → X)
\end{code}
Added 31 October 2022 by Tom de Jong.
We record the (computational) behaviour of transfinite induction on OO for use
in other constructions.
\begin{code}
transfinite-induction-on-OO-behaviour :
(P : Ordinal 𝓤 → 𝓥 ̇ )
→ (f : (α : Ordinal 𝓤) → ((a : ⟨ α ⟩) → P (α ↓ a)) → P α)
→ (α : Ordinal 𝓤) → transfinite-induction-on-OO P f α
＝ f α (λ a → transfinite-induction-on-OO P f (α ↓ a))
transfinite-induction-on-OO-behaviour {𝓤} {𝓥} P f =
Transfinite-induction-behaviour fe (OO 𝓤) P f'
where
f' : (α : Ordinal 𝓤)
→ ((α' : Ordinal 𝓤) → α' ⊲ α → P α')
→ P α
f' α g = f α (λ a → g (α ↓ a) (a , refl))
transfinite-recursion-on-OO-behaviour :
(X : 𝓥 ̇ )
→ (f : (α : Ordinal 𝓤) → (⟨ α ⟩ → X) → X)
→ (α : Ordinal 𝓤) → transfinite-recursion-on-OO X f α
＝ f α (λ a → transfinite-recursion-on-OO X f (α ↓ a))
transfinite-recursion-on-OO-behaviour X f =
transfinite-induction-on-OO-behaviour (λ _ → X) f
\end{code}
End of addition.
\begin{code}
has-minimal-element : Ordinal 𝓤 → 𝓤 ̇
has-minimal-element α = Σ a ꞉ ⟨ α ⟩ , ((x : ⟨ α ⟩) → a ≾⟨ α ⟩ x)
has-no-minimal-element : Ordinal 𝓤 → 𝓤 ̇
has-no-minimal-element α = ((a : ⟨ α ⟩) → ¬¬ (Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a))
ordinal-with-no-minimal-element-is-empty : (α : Ordinal 𝓤)
→ has-no-minimal-element α
→ is-empty ⟨ α ⟩
ordinal-with-no-minimal-element-is-empty {𝓤} = transfinite-induction-on-OO P ϕ
where
P : Ordinal 𝓤 → 𝓤 ̇
P α = has-no-minimal-element α → is-empty ⟨ α ⟩
ϕ : (α : Ordinal 𝓤) → ((a : ⟨ α ⟩) → P (α ↓ a)) → P α
ϕ α f g x = g x (f x h)
where
h : has-no-minimal-element (α ↓ x)
h (y , l) u = g y (contrapositive k u)
where
k : ⟨ α ↓ y ⟩ → ⟨ (α ↓ x) ↓ (y , l) ⟩
k (z , m) = (z , o) , m
where
o : z ≺⟨ α ⟩ x
o = Transitivity α z y x m l
non-empty-classically-has-minimal-element : (α : Ordinal 𝓤)
→ is-nonempty ⟨ α ⟩
→ ¬¬ has-minimal-element α
non-empty-classically-has-minimal-element {𝓤} α n = iv
where
i : ¬ has-no-minimal-element α
i = contrapositive (ordinal-with-no-minimal-element-is-empty α) n
ii : ¬¬ (Σ a ꞉ ⟨ α ⟩ , ¬ (Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a))
ii = not-Π-not-not-implies-not-not-Σ-not i
iii : (Σ a ꞉ ⟨ α ⟩ , ¬ (Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a))
→ (Σ a ꞉ ⟨ α ⟩ , ((x : ⟨ α ⟩) → a ≾⟨ α ⟩ x))
iii (a , n) = a , not-Σ-implies-Π-not n
iv : ¬¬ (Σ a ꞉ ⟨ α ⟩ , ((x : ⟨ α ⟩) → a ≾⟨ α ⟩ x))
iv = ¬¬-functor iii ii
NB-minimal : (α : Ordinal 𝓤) (a : ⟨ α ⟩)
→ ((x : ⟨ α ⟩) → a ≾⟨ α ⟩ x)
⇔ ((x : ⟨ α ⟩) → a ≼⟨ α ⟩ x)
NB-minimal α a = f , g
where
f : ((x : ⟨ α ⟩) → a ≾⟨ α ⟩ x) → ((x : ⟨ α ⟩) → a ≼⟨ α ⟩ x)
f h x u l = 𝟘-elim (h u l)
g : ((x : ⟨ α ⟩) → a ≼⟨ α ⟩ x) → ((x : ⟨ α ⟩) → a ≾⟨ α ⟩ x)
g k x m = irrefl α x (k x x m)
\end{code}
Added 29th March 2022.
Simulations preserve least elements.
\begin{code}
initial-segments-preserve-least : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(x : ⟨ α ⟩) (y : ⟨ β ⟩)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-initial-segment α β f
→ is-least α x
→ is-least β y
→ f x ＝ y
initial-segments-preserve-least α β x y f i m n = c
where
a : f x ≼⟨ β ⟩ y
a u l = IV
where
x' : ⟨ α ⟩
x' = pr₁ (i x u l)
I : x' ≺⟨ α ⟩ x
I = pr₁ (pr₂ (i x u l))
II : x ≼⟨ α ⟩ x'
II = m x'
III : x' ≺⟨ α ⟩ x'
III = II x' I
IV : u ≺⟨ β ⟩ y
IV = 𝟘-elim (irrefl α x' III)
b : y ≼⟨ β ⟩ f x
b = n (f x)
c : f x ＝ y
c = Antisymmetry β (f x) y a b
simulations-preserve-least : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(x : ⟨ α ⟩) (y : ⟨ β ⟩)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-least α x
→ is-least β y
→ f x ＝ y
simulations-preserve-least α β x y f (i , _) = initial-segments-preserve-least α β x y f i
\end{code}
Added 2nd May 2022 by Martin Escardo.
\begin{code}
order-preserving-gives-not-⊲ : (α β : Ordinal 𝓤)
→ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-order-preserving α β f)
→ ¬ (β ⊲ α)
order-preserving-gives-not-⊲ {𝓤} α β σ (x₀ , refl) = γ σ
where
γ : ¬ (Σ f ꞉ (⟨ α ⟩ → ⟨ α ↓ x₀ ⟩) , is-order-preserving α (α ↓ x₀) f)
γ (f , fop) = κ
where
g : ⟨ α ⟩ → ⟨ α ⟩
g x = pr₁ (f x)
h : (x : ⟨ α ⟩) → g x ≺⟨ α ⟩ x₀
h x = pr₂ (f x)
δ : (n : ℕ) → (g ^ succ n) x₀ ≺⟨ α ⟩ (g ^ n) x₀
δ 0 = h x₀
δ (succ n) = fop _ _ (δ n)
A : ⟨ α ⟩ → 𝓤 ̇
A x = Σ n ꞉ ℕ , (g ^ n) x₀ ＝ x
d : (x : ⟨ α ⟩) → A x → Σ y ꞉ ⟨ α ⟩ , (y ≺⟨ α ⟩ x) × A y
d x (n , refl) = g x , δ n , succ n , refl
κ : 𝟘
κ = no-minimal-is-empty' (underlying-order α) (Well-foundedness α)
A d (x₀ , 0 , refl)
open import UF.ExcludedMiddle
order-preserving-gives-≼ : EM (𝓤 ⁺)
→ (α β : Ordinal 𝓤)
→ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-order-preserving α β f)
→ α ≼ β
order-preserving-gives-≼ em α β σ = δ
where
γ : (α ≼ β) + (β ⊲ α) → α ≼ β
γ (inl l) = l
γ (inr m) = 𝟘-elim (order-preserving-gives-not-⊲ α β σ m)
δ : α ≼ β
δ = γ (≼-or-> _⊲_ fe' em ⊲-is-well-order α β)
\end{code}
Added in March 2022 by Tom de Jong:
Notice that we defined "is-initial-segment" using Σ (rather than ∃). This is
fine, because if f is a simulation from α to β, then for every x : ⟨ α ⟩ and
y : ⟨ β ⟩ with y ≺⟨ β ⟩ f x, the type (Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y))
is a proposition. It follows (see the proof above) that being a simulation is
property.
However, for some purposes, notably for constructing suprema of ordinals in
OrdinalSupOfOrdinals.lagda, it is useful to formulate the notion of initial
segment and the notion of simulation using ∃, rather than Σ.
Using the techniques that were used above to prove that being a simulation is
property, we show the definition of simulation with ∃ to be equivalent to the
original one.
\begin{code}
open import UF.PropTrunc
module _ (pt : propositional-truncations-exist) where
open PropositionalTruncation pt
is-initial-segment' : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇
is-initial-segment' α β f = (x : ⟨ α ⟩) (y : ⟨ β ⟩)
→ y ≺⟨ β ⟩ f x
→ ∃ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y)
is-simulation' : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇
is-simulation' α β f = is-initial-segment' α β f × is-order-preserving α β f
simulations-are-lc' : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation' α β f
→ left-cancellable f
simulations-are-lc' α β f (i , p) = γ
where
φ : ∀ x y
→ is-accessible (underlying-order α) x
→ is-accessible (underlying-order α) y
→ f x ＝ f y
→ x ＝ y
φ x y (step s) (step t) r = Extensionality α x y g h
where
g : (u : ⟨ α ⟩) → u ≺⟨ α ⟩ x → u ≺⟨ α ⟩ y
g u l = ∥∥-rec (Prop-valuedness α u y) b (i y (f u) a)
where
a : f u ≺⟨ β ⟩ f y
a = transport (λ - → f u ≺⟨ β ⟩ -) r (p u x l)
b : (Σ v ꞉ ⟨ α ⟩ , (v ≺⟨ α ⟩ y) × (f v ＝ f u))
→ u ≺⟨ α ⟩ y
b (v , k , e) = transport (λ - → - ≺⟨ α ⟩ y) (c ⁻¹) k
where
c : u ＝ v
c = φ u v (s u l) (t v k) (e ⁻¹)
h : (u : ⟨ α ⟩) → u ≺⟨ α ⟩ y → u ≺⟨ α ⟩ x
h u l = ∥∥-rec (Prop-valuedness α u x) b (i x (f u) a)
where
a : f u ≺⟨ β ⟩ f x
a = transport (λ - → f u ≺⟨ β ⟩ -) (r ⁻¹) (p u y l)
b : (Σ v ꞉ ⟨ α ⟩ , (v ≺⟨ α ⟩ x) × (f v ＝ f u))
→ u ≺⟨ α ⟩ x
b (v , k , e) = transport (λ - → - ≺⟨ α ⟩ x) c k
where
c : v ＝ u
c = φ v u (s v k) (t u l) e
γ : left-cancellable f
γ {x} {y} = φ x y (Well-foundedness α x) (Well-foundedness α y)
simulation-prime : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation α β f
→ is-simulation' α β f
simulation-prime α β f (i , p) = (j , p)
where
j : is-initial-segment' α β f
j x y l = ∣ i x y l ∣
simulation-unprime : (α : Ordinal 𝓤) (β : Ordinal 𝓥)
(f : ⟨ α ⟩ → ⟨ β ⟩)
→ is-simulation' α β f
→ is-simulation α β f
simulation-unprime α β f (i , p) = (j , p)
where
j : is-initial-segment α β f
j x y l = ∥∥-rec prp id (i x y l)
where
prp : is-prop (Σ x' ꞉ ⟨ α ⟩ , (x' ≺⟨ α ⟩ x) × (f x' ＝ y))
prp (z , l , e) (z' , l' , e') = to-subtype-＝ ⦅1⦆ ⦅2⦆
where
⦅1⦆ : (x' : ⟨ α ⟩) → is-prop ((x' ≺⟨ α ⟩ x) × (f x' ＝ y))
⦅1⦆ x' = ×-is-prop (Prop-valuedness α x' x) (underlying-type-is-set fe β)
⦅2⦆ : z ＝ z'
⦅2⦆ = simulations-are-lc' α β f (i , p) (e ∙ e' ⁻¹)
\end{code}