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 --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-} 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 UF.Base 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 𝓤 𝓥 \end{code} The simulations make the ordinals into a poset: \begin{code} _⊴_ : 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 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) ⊴-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-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 \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 (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 (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 (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} 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} 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.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 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} 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} 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}