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 OrdinalOfOrdinals
(ua : Univalence)
where
open import SpartanMLTT
open import OrdinalNotions
open import OrdinalsType
open import CanonicalMapNotation
open import UF-Base
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-Embeddings
open import UF-FunExt
open import UF-Equiv
open import UF-Equiv-FunExt
open import UF-UA-FunExt
open import UF-Yoneda
open import UF-EquivalenceExamples
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ₒ α β
\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 LPO fe
open import OrdinalArithmetic fe
open import GenericConvergentSequence
open import NaturalsOrder
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}
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)
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-Π-implies-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}