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 used to show that (1) the type of ordinals forms a (large)
set, (2) its order is extensional, (3) hence it is itself a (large)
ordinal, (4) the type of ordinals is locally small.
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import UF.Univalence
module Ordinals.OrdinalOfOrdinals
(ua : Univalence)
where
open import MLTT.Spartan
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Notions
open import Ordinals.Type
open import Ordinals.Underlying
open import Ordinals.WellOrderTransport
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Subsingletons
open import UF.UA-FunExt
private
fe : FunExt
fe = Univalence-gives-FunExt ua
fe' : Fun-Ext
fe' {𝓤} {𝓥} = fe 𝓤 𝓥
open import Ordinals.Arithmetic fe
\end{code}
The simulations make the ordinals into a poset:
\begin{code}
_⊴_ : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇
α ⊴ β = Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-simulation α β f
[_,_]⟨_⟩ : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → α ⊴ β → ⟨ α ⟩ → ⟨ β ⟩
[ α , β ]⟨ f ⟩ = pr₁ f
[_,_]⟨_⟩-is-simulation : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : α ⊴ β)
→ is-simulation α β [ α , β ]⟨ f ⟩
[_,_]⟨_⟩-is-simulation α β f = pr₂ f
⊴-gives-↪ : (α : Ordinal 𝓤)
(β : Ordinal 𝓥)
→ α ⊴ β
→ ⟨ α ⟩ ↪ ⟨ β ⟩
⊴-gives-↪ α β (f , s) = f , simulations-are-embeddings fe α β f s
⊴-is-prop-valued : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → is-prop (α ⊴ β)
⊴-is-prop-valued {𝓤} {𝓥} α β (f , s) (g , t) =
to-subtype-＝
(being-simulation-is-prop fe' α β)
(dfunext fe' (at-most-one-simulation α β f g s t))
⊴-refl : (α : Ordinal 𝓤) → α ⊴ α
⊴-refl α = id ,
(λ x z l → z , l , refl) ,
(λ x y l → l)
＝-to-⊴ : (α β : Ordinal 𝓤) → α ＝ β → α ⊴ β
＝-to-⊴ α β refl = ⊴-refl α
⊴-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))
≃ₒ-to-⊴ : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → α ≃ₒ β → α ⊴ β
≃ₒ-to-⊴ α β (f , e) = (f , order-equivs-are-simulations α β f e)
ordinal-equiv-gives-bisimilarity : (α : Ordinal 𝓤) (β : 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 𝓤) (β : 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
\end{code}
A corollary of the above is that the ordinal order _⊴_ is
antisymmetric.
\begin{code}
⊴-antisym : (α β : Ordinal 𝓤)
→ α ⊴ β
→ β ⊴ α
→ α ＝ β
⊴-antisym α β l m =
eqtoidₒ (ua _) fe' α β (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 (acc s) l = acc (λ σ 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
segment-inclusion-lc : (α : Ordinal 𝓤) {a : ⟨ α ⟩}
→ left-cancellable (segment-inclusion α a)
segment-inclusion-lc α {a} =
simulations-are-lc (α ↓ 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))))
↓-is-embedding : (α : Ordinal 𝓤) → is-embedding (α ↓_)
↓-is-embedding α = lc-maps-into-sets-are-embeddings
(α ↓_)
(↓-lc α _ _)
(the-type-of-ordinals-is-a-set (ua _) fe')
\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 (ua 𝓤) fe') 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ₒ-≃ (ua _) fe' α (β ↓ 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 (acc s) = acc 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 {𝓤} α = acc 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)⁻¹)
OO-⊴-next-OO : OO 𝓤 ⊴ OO (𝓤 ⁺)
OO-⊴-next-OO {𝓤} = ordinals-in-OO-are-embedded-in-OO (OO 𝓤)
ordinals-are-embedded-in-Ordinal : (α : Ordinal 𝓤) → ⟨ α ⟩ ↪ Ordinal 𝓤
ordinals-are-embedded-in-Ordinal {𝓤} α = ⊴-gives-↪ α (OO 𝓤)
(ordinals-in-OO-are-embedded-in-OO α)
Ordinal-embedded-in-next-Ordinal : Ordinal 𝓤 ↪ Ordinal (𝓤 ⁺)
Ordinal-embedded-in-next-Ordinal {𝓤} = ordinals-are-embedded-in-Ordinal (OO 𝓤)
\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}
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ₒ (ua _) fe' (α ↓ 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 9 September 2024 by Tom de Jong and Fredrik Nordvall Forsberg.
\begin{code}
⊲-⊴-gives-⊲ : (α β γ : Ordinal 𝓤) → α ⊲ β → β ⊴ γ → α ⊲ γ
⊲-⊴-gives-⊲ α β γ l k = ≼-trans _⊲_ (⊴-gives-≼ β γ k) (≼-refl _⊲_) α l
\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)
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 2nd May 2022.
\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.ClassicalLogic
EM-implies-order-preserving-gives-≼ : EM 𝓤
→ (α β : Ordinal 𝓤)
→ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-order-preserving α β f)
→ α ≼ β
EM-implies-order-preserving-gives-≼ em α β σ = δ
where
γ : (∀ u → u ⊲⁻ α → u ⊲⁻ β) + (β ⊲⁻ α) → α ≼ β
γ (inl l) γ p = ⌜ ⊲-is-equivalent-to-⊲⁻ γ β ⌝⁻¹ (l γ (⌜ ⊲-is-equivalent-to-⊲⁻ γ α ⌝ p))
γ (inr m) = 𝟘-elim (order-preserving-gives-not-⊲ α β σ (⌜ ⊲-is-equivalent-to-⊲⁻ β α ⌝⁻¹ m))
⊲⁻-is-well-order : is-well-order {𝓤 ⁺} {𝓤} _⊲⁻_
⊲⁻-is-well-order {𝓤} = order-transfer-lemma₃.well-order→ fe (Ordinal 𝓤) _⊲_ _⊲⁻_
⊲-is-equivalent-to-⊲⁻
⊲-is-well-order
δ : α ≼ β
δ = γ (≼-or-> _⊲⁻_ fe' em ⊲⁻-is-well-order α β)
\end{code}
Added 19 November 2024 by Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
and Tom de Jong.
In fact order preserving maps can be upgraded to inequalities if and
only if excluded middle holds.
\begin{code}
order-preserving-gives-≼-implies-EM :
((α β : Ordinal 𝓤)
→ Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-order-preserving α β f
→ α ≼ β)
→ EM 𝓤
order-preserving-gives-≼-implies-EM h P P-is-prop = II (g ⋆) refl
where
open import MLTT.Plus-Properties
α = 𝟙ₒ
Pₒ = prop-ordinal P P-is-prop
β = Pₒ +ₒ 𝟙ₒ
f : ⟨ α ⟩ → ⟨ β ⟩
f ⋆ = inr ⋆
f-is-order-preserving : is-order-preserving α β f
f-is-order-preserving ⋆ ⋆ = 𝟘-elim
𝕘 : α ⊴ β
𝕘 = ≼-gives-⊴ α β (h α β (f , f-is-order-preserving))
g = [ α , β ]⟨ 𝕘 ⟩
inl-p-is-least : (p : P) → is-least β (inl p)
inl-p-is-least p (inl _) (inl _) l = l
inl-p-is-least p (inl _) (inr _) l = l
inl-p-is-least p (inr _) (inl _) l = ⋆
inl-p-is-least p (inr _) (inr _) l = l
I : (p : P) → g ⋆ ＝ inl p
I p = simulations-preserve-least α β ⋆ (inl p)
g ([ α , β ]⟨ 𝕘 ⟩-is-simulation)
(λ ⋆ ⋆ → 𝟘-elim) (inl-p-is-least p)
II : (y : ⟨ β ⟩) → g ⋆ ＝ y → P + ¬ P
II (inl p) e = inl p
II (inr ⋆) e = inr (λ p → +disjoint ((I p) ⁻¹ ∙ e))
\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)
Idtofunₒ-↓-lemma : {α β : Ordinal 𝓤} {a : ⟨ α ⟩}
(e : α ＝ β)
→ α ↓ a ＝ β ↓ Idtofunₒ e a
Idtofunₒ-↓-lemma refl = refl
\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}
abstract
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
transfinite-recursion-on-OO-bundled :
(X : 𝓥 ̇ )
→ (f : (α : Ordinal 𝓤) → (⟨ α ⟩ → X) → X)
→ Σ r ꞉ (Ordinal 𝓤 → X) , ((α : Ordinal 𝓤) → r α ＝ f α (λ a → r (α ↓ a)))
transfinite-recursion-on-OO-bundled X f =
transfinite-recursion-on-OO X f , transfinite-recursion-on-OO-behaviour X f
\end{code}
Added 1st June 2023 by Martin Escardo.
\begin{code}
definition-by-transfinite-recursion-on-OO :
(X : 𝓥 ̇ )
→ (f : (α : Ordinal 𝓤) → (⟨ α ⟩ → X) → X)
→ Σ h ꞉ (Ordinal 𝓤 → X) , (∀ α → h α ＝ f α (λ a → h (α ↓ a)))
definition-by-transfinite-recursion-on-OO X f =
transfinite-recursion-on-OO X f ,
transfinite-recursion-on-OO-behaviour X f
definition-by-transfinite-induction-on-OO :
(X : Ordinal 𝓤 → 𝓥 ̇ )
→ (f : (α : Ordinal 𝓤) → ((a : ⟨ α ⟩) → X (α ↓ a)) → X α)
→ Σ h ꞉ ((α : Ordinal 𝓤) → X α) , (∀ α → h α ＝ f α (λ a → h (α ↓ a)))
definition-by-transfinite-induction-on-OO X f =
transfinite-induction-on-OO X f ,
transfinite-induction-on-OO-behaviour X f
\end{code}
Added 4 June 2024 at the Hausdorff Reseach Institute for Mathematics (HIM).
By Tom de Jong and Fredrik Nordvall Forsberg.
Given simulations
f : α ⊴ γ and g : β ⊴ γ
and points a : α and b : β we have
f a ≼ g b ⇔ α ↓ a ⊴ β ↓ b,
and
f a ＝ g b ⇔ α ↓ a ≃ₒ β ↓ b.
\begin{code}
initial-segments-⊴-gives-simulations-pointwise-≼ :
(α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦)
(f : α ⊴ γ) (g : β ⊴ γ)
(a : ⟨ α ⟩) (b : ⟨ β ⟩)
→ (α ↓ a) ⊴ (β ↓ b)
→ [ α , γ ]⟨ f ⟩ a ≼⟨ γ ⟩ [ β , γ ]⟨ g ⟩ b
initial-segments-⊴-gives-simulations-pointwise-≼
α β γ 𝕗@(f , f-sim) 𝕘@(g , g-sim) a b 𝕖@(e , e-sim) c c-below-fa = V
where
I : Σ x ꞉ ⟨ α ⟩ , x ≺⟨ α ⟩ a × (f x ＝ c)
I = simulations-are-initial-segments α γ f f-sim a c c-below-fa
x : ⟨ α ⟩
x = pr₁ I
x-below-a : x ≺⟨ α ⟩ a
x-below-a = pr₁ (pr₂ I)
fx-equals-c : f x ＝ c
fx-equals-c = pr₂ (pr₂ I)
II : ⟨ β ↓ b ⟩
II = e (x , x-below-a)
y : ⟨ β ⟩
y = pr₁ II
y-below-b : y ≺⟨ β ⟩ b
y-below-b = pr₂ II
\end{code}
We now prove that f x ＝ g y by considering the necessarily commutative
diagram of simulations
α ↓ a ⊴ β ↓ b
⊴ ⊴
α β
⊴ᶠ ᵍ⊵
γ
\begin{code}
III : f x ＝ g y
III = ap (λ - → pr₁ - (x , x-below-a)) sim-commute
where
sim-commute :
⊴-trans (α ↓ a) α γ (segment-⊴ α a) 𝕗
＝ ⊴-trans (α ↓ a) (β ↓ b) γ 𝕖 (⊴-trans (β ↓ b) β γ (segment-⊴ β b) 𝕘)
sim-commute =
⊴-is-prop-valued (α ↓ a) γ
(⊴-trans (α ↓ a) α γ (segment-⊴ α a) 𝕗)
(⊴-trans (α ↓ a) (β ↓ b) γ 𝕖 (⊴-trans (β ↓ b) β γ (segment-⊴ β b) 𝕘))
IV : c ＝ g y
IV = fx-equals-c ⁻¹ ∙ III
V : c ≺⟨ γ ⟩ g b
V = transport⁻¹ (λ - → - ≺⟨ γ ⟩ g b) IV
(simulations-are-order-preserving β γ g g-sim y b y-below-b)
isomorphic-initial-segments-gives-simulations-pointwise-equal :
(α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦)
(f : α ⊴ γ) (g : β ⊴ γ)
(a : ⟨ α ⟩) (b : ⟨ β ⟩)
→ (α ↓ a) ≃ₒ (β ↓ b)
→ (pr₁ f) a ＝ (pr₁ g) b
isomorphic-initial-segments-gives-simulations-pointwise-equal α β γ f g a b e =
Extensionality γ (pr₁ f a) (pr₁ g b) I II
where
I : pr₁ f a ≼⟨ γ ⟩ pr₁ g b
I = initial-segments-⊴-gives-simulations-pointwise-≼ α β γ f g a b
(≃ₒ-to-⊴ (α ↓ a) (β ↓ b) e)
II : pr₁ g b ≼⟨ γ ⟩ pr₁ f a
II = initial-segments-⊴-gives-simulations-pointwise-≼ β α γ g f b a
(≃ₒ-to-⊴ (β ↓ b) (α ↓ a) (≃ₒ-sym (α ↓ a) (β ↓ b) e))
\end{code}
We illustrate the above lemmas by showing that they generalize the
left-cancellability of taking initial segments (which was already proved above).
\begin{code}
↓-⊴-lc-bis : (α : Ordinal 𝓤) (a b : ⟨ α ⟩)
→ (α ↓ a) ⊴ (α ↓ b )
→ a ≼⟨ α ⟩ b
↓-⊴-lc-bis α =
initial-segments-⊴-gives-simulations-pointwise-≼ α α α (⊴-refl α) (⊴-refl α)
↓-lc-bis : (α : Ordinal 𝓤) (a b : ⟨ α ⟩)
→ (α ↓ a) ≃ₒ (α ↓ b )
→ a ＝ b
↓-lc-bis α =
isomorphic-initial-segments-gives-simulations-pointwise-equal α α α
(⊴-refl α) (⊴-refl α)
\end{code}
We now prove the converses to the above lemmas.
\begin{code}
simulations-pointwise-≼-gives-initial-segments-⊴ :
(α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦)
(f : α ⊴ γ) (g : β ⊴ γ)
(a : ⟨ α ⟩) (b : ⟨ β ⟩)
→ (pr₁ f) a ≼⟨ γ ⟩ (pr₁ g) b
→ (α ↓ a) ⊴ (β ↓ b)
simulations-pointwise-≼-gives-initial-segments-⊴
α β γ 𝕗@(f , f-sim) 𝕘@(g , g-sim) a b fa-below-gb = h ,
h-intial-segment ,
h-order-preserving
where
h-prelim : (x : ⟨ α ⟩)
→ x ≺⟨ α ⟩ a
→ Σ y ꞉ ⟨ β ⟩ , (y ≺⟨ β ⟩ b) × (g y ＝ f x)
h-prelim x l = simulations-are-initial-segments β γ g g-sim b (f x) l'
where
l' : f x ≺⟨ γ ⟩ g b
l' = fa-below-gb (f x) (simulations-are-order-preserving α γ f f-sim x a l)
h : ⟨ α ↓ a ⟩ → ⟨ β ↓ b ⟩
h (x , l) = (pr₁ (h-prelim x l) , pr₁ (pr₂ (h-prelim x l)))
h̅ : ⟨ α ↓ a ⟩ → ⟨ β ⟩
h̅ = segment-inclusion β b ∘ h
h-eq : (x : ⟨ α ⟩) (l : x ≺⟨ α ⟩ a)
→ g (h̅ (x , l)) ＝ f x
h-eq x l = pr₂ (pr₂ (h-prelim x l))
h-order-preserving : is-order-preserving (α ↓ a) (β ↓ b) h
h-order-preserving (x , l) (y , k) x-below-y = III
where
I : f x ≺⟨ γ ⟩ f y
I = simulations-are-order-preserving α γ f f-sim x y x-below-y
II : g (h̅ (x , l)) ≺⟨ γ ⟩ g (h̅ (y , k))
II = transport₂⁻¹ (underlying-order γ) (h-eq x l) (h-eq y k) I
III : h̅ (x , l) ≺⟨ β ⟩ h̅ (y , k)
III = simulations-are-order-reflecting β γ g g-sim
(h̅ (x , l)) (h̅ (y , k)) II
h-intial-segment : is-initial-segment (α ↓ a) (β ↓ b) h
h-intial-segment (x , l) (y , k) y-below-hx = (x' , IV) , x'-below-x , V
where
I : g y ≺⟨ γ ⟩ g (h̅ (x , l))
I = simulations-are-order-preserving β γ g g-sim y (h̅ (x , l)) y-below-hx
II : g y ≺⟨ γ ⟩ f x
II = transport (λ - → g y ≺⟨ γ ⟩ -) (h-eq x l) I
III : Σ x' ꞉ ⟨ α ⟩ , x' ≺⟨ α ⟩ x × (f x' ＝ g y)
III = simulations-are-initial-segments α γ f f-sim x (g y) II
x' : ⟨ α ⟩
x' = pr₁ III
x'-below-x : x' ≺⟨ α ⟩ x
x'-below-x = pr₁ (pr₂ III)
IV : x' ≺⟨ α ⟩ a
IV = Transitivity α x' x a x'-below-x l
V : h (x' , IV) ＝ y , k
V = to-subtype-＝ (λ _ → Prop-valuedness β _ b)
(simulations-are-lc β γ g g-sim
(g (h̅ (x' , IV)) ＝⟨ h-eq x' IV ⟩
f x' ＝⟨ pr₂ (pr₂ III) ⟩
g y ∎))
simulations-pointwise-equal-gives-isomorphic-initial-segments :
(α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦)
(f : α ⊴ γ) (g : β ⊴ γ)
(a : ⟨ α ⟩) (b : ⟨ β ⟩)
→ (pr₁ f) a ＝ (pr₁ g) b
→ (α ↓ a) ≃ₒ (β ↓ b)
simulations-pointwise-equal-gives-isomorphic-initial-segments α β γ f g a b eq =
bisimilarity-gives-ordinal-equiv (α ↓ a) (β ↓ b) I II
where
I : (α ↓ a) ⊴ (β ↓ b)
I = simulations-pointwise-≼-gives-initial-segments-⊴ α β γ f g a b
(≼-refl-＝ (underlying-order γ) eq)
II : (β ↓ b) ⊴ (α ↓ a)
II = simulations-pointwise-≼-gives-initial-segments-⊴ β α γ g f b a
(≼-refl-＝ (underlying-order γ) (eq ⁻¹))
\end{code}
Fixities and precedences
\begin{code}
infix 4 _⊲_
infix 4 _⊴_
infixl 5 _↓_
\end{code}