Martin Escardo, 29 June 2018, 26th February 2023 Equivalence of ordinals. \begin{code} {-# OPTIONS --safe --without-K #-} open import MLTT.Spartan open import Ordinals.Maps open import Ordinals.Notions open import Ordinals.Type open import Ordinals.Underlying 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.PreSIP-Examples open import UF.PreUnivalence open import UF.Sets open import UF.Size open import UF.Subsingletons open import UF.Univalence open import UF.Yoneda module Ordinals.Equivalence where \end{code} Characterization of equality of ordinals using the structure identity principle: \begin{code} Ordinal-= : FunExt → is-univalent 𝓤 → (α β : Ordinal 𝓤) → (α = β) ≃ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-equiv f × ((λ x x' → x ≺⟨ α ⟩ x') = (λ x x' → f x ≺⟨ β ⟩ f x'))) Ordinal-= {𝓤} fe = generalized-metric-space.characterization-of-M-= (𝓤 ̇ ) (λ _ → is-well-order) (λ X _<_ → being-well-order-is-prop _<_ fe) where open import UF.SIP-Examples \end{code} Often it is convenient to work with the following alternative notion _≃ₒ_ of ordinal equivalence, which we take as the official one: \begin{code} is-order-equiv : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (⟨ α ⟩ → ⟨ β ⟩) → 𝓤 ⊔ 𝓥 ̇ is-order-equiv α β f = is-order-preserving α β f × (Σ e ꞉ is-equiv f , is-order-preserving β α (inverse f e)) order-equivs-are-order-preserving : (α : Ordinal 𝓤) (β : Ordinal 𝓥) {f : ⟨ α ⟩ → ⟨ β ⟩} → is-order-equiv α β f → is-order-preserving α β f order-equivs-are-order-preserving α β = pr₁ order-equivs-are-equivs : (α : Ordinal 𝓤) (β : Ordinal 𝓥) {f : ⟨ α ⟩ → ⟨ β ⟩} → (i : is-order-equiv α β f) → is-equiv f order-equivs-are-equivs α β = pr₁ ∘ pr₂ inverses-of-order-equivs-are-order-preserving : (α : Ordinal 𝓤) (β : Ordinal 𝓥) {f : ⟨ α ⟩ → ⟨ β ⟩} → (i : is-order-equiv α β f) → is-order-preserving β α (inverse f (order-equivs-are-equivs α β i)) inverses-of-order-equivs-are-order-preserving α β = pr₂ ∘ pr₂ being-order-equiv-is-prop : Fun-Ext → (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : ⟨ α ⟩ → ⟨ β ⟩) → is-prop (is-order-equiv α β f) being-order-equiv-is-prop fe α β f = ×-is-prop (being-order-preserving-is-prop fe α β f) (Σ-is-prop (being-equiv-is-prop (λ _ _ → fe) f) (λ e → being-order-preserving-is-prop fe β α (inverse f e))) \end{code} Our official definition of ordinal equivalence (see below for equivalent definitions): \begin{code} _≃ₒ_ : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇ α ≃ₒ β = Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-order-equiv α β f ≃ₒ-refl : (α : Ordinal 𝓤) → α ≃ₒ α ≃ₒ-refl α = id , (λ x y → id) , id-is-equiv ⟨ α ⟩ , (λ x y → id) idtoeqₒ : (α β : Ordinal 𝓤) → α = β → α ≃ₒ β idtoeqₒ α α refl = ≃ₒ-refl α eqtoidₒ : is-univalent 𝓤 → Fun-Ext → (α β : Ordinal 𝓤) → α ≃ₒ β → α = β eqtoidₒ {𝓤} ua fe α β (f , p , e , q) = γ where abstract 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 \end{code} For historical reasons, the above proof doesn't use the structure identity principle. \begin{code} ≃ₒ-sym : (α : Ordinal 𝓤) (β : Ordinal 𝓥 ) → α ≃ₒ β → β ≃ₒ α ≃ₒ-sym α β (f , p , e , q) = inverse f e , q , inverses-are-equivs f e , p ≃ₒ-trans : ∀ {𝓤} {𝓥} {𝓦} (α : Ordinal 𝓤) (β : Ordinal 𝓥 ) (γ : Ordinal 𝓦) → α ≃ₒ β → β ≃ₒ γ → α ≃ₒ γ ≃ₒ-trans α β γ (f , p , e , q) (f' , p' , e' , q') = f' ∘ f , (λ x y l → p' (f x) (f y) (p x y l)) , ∘-is-equiv e e' , (λ x y l → q (inverse f' e' x) (inverse f' e' y) (q' x y l)) 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 ≃ₒ-to-fun : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → α ≃ₒ β → ⟨ α ⟩ → ⟨ β ⟩ ≃ₒ-to-fun α β = pr₁ ≃ₒ-to-fun-is-order-equiv : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (e : α ≃ₒ β) → is-order-equiv α β (≃ₒ-to-fun α β e) ≃ₒ-to-fun-is-order-equiv α β = pr₂ ≃ₒ-to-fun-is-equiv : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (e : α ≃ₒ β) → is-equiv (≃ₒ-to-fun α β e) ≃ₒ-to-fun-is-equiv α β e = order-equivs-are-equivs α β (≃ₒ-to-fun-is-order-equiv α β e) order-preserving-reflecting-equivs-are-order-equivs : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : ⟨ α ⟩ → ⟨ β ⟩) → is-equiv f → is-order-preserving α β f → is-order-reflecting α β f → is-order-equiv α β f order-preserving-reflecting-equivs-are-order-equivs α β f e p r = p , e , order-reflecting-gives-inverse-order-preserving α β f e r order-equivs-are-order-reflecting : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (f : ⟨ α ⟩ → ⟨ β ⟩) → is-order-equiv α β f → is-order-reflecting α β f order-equivs-are-order-reflecting α β f (_ , e , q) = inverse-order-reflecting-gives-order-preserving α β f e q inverses-of-order-equivs-are-order-reflecting : (α : Ordinal 𝓤) (β : Ordinal 𝓥) {f : ⟨ α ⟩ → ⟨ β ⟩} → (i : is-order-equiv α β f) → is-order-reflecting β α (inverse f (order-equivs-are-equivs α β i)) inverses-of-order-equivs-are-order-reflecting α β {f} (p , e , q) = order-equivs-are-order-reflecting β α (inverse f e) (q , inverses-are-equivs f e , p) inverses-of-order-equivs-are-order-equivs : (α : Ordinal 𝓤) (β : Ordinal 𝓥) {f : ⟨ α ⟩ → ⟨ β ⟩} → (i : is-order-equiv α β f) → is-order-equiv β α (inverse f (order-equivs-are-equivs α β i)) inverses-of-order-equivs-are-order-equivs α β {f} (p , e , q) = (q , inverses-are-equivs f e , p) ≃ₒ-to-fun⁻¹ : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → α ≃ₒ β → ⟨ β ⟩ → ⟨ α ⟩ ≃ₒ-to-fun⁻¹ α β e = inverse (≃ₒ-to-fun α β e) (order-equivs-are-equivs α β (≃ₒ-to-fun-is-order-equiv α β e)) ≃ₒ-to-fun⁻¹-is-equiv : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (e : α ≃ₒ β) → is-equiv (≃ₒ-to-fun⁻¹ α β e) ≃ₒ-to-fun⁻¹-is-equiv α β e = inverses-are-equivs (≃ₒ-to-fun α β e) (≃ₒ-to-fun-is-equiv α β e) ≃ₒ-gives-≃ : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → α ≃ₒ β → ⟨ α ⟩ ≃ ⟨ β ⟩ ≃ₒ-gives-≃ α β (f , p , e , q) = (f , e) ≃ₒ-is-prop-valued : Fun-Ext → (α : Ordinal 𝓤) (β : Ordinal 𝓥) → is-prop (α ≃ₒ β) ≃ₒ-is-prop-valued fe α β (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 fe α β) (dfunext fe r) UAₒ : is-univalent 𝓤 → Fun-Ext → (α β : Ordinal 𝓤) → is-equiv (idtoeqₒ α β) UAₒ {𝓤} ua fe α = nats-with-sections-are-equivs α (idtoeqₒ α) (λ β → (eqtoidₒ ua fe α β , η β)) where η : (β : Ordinal 𝓤) (e : α ≃ₒ β) → idtoeqₒ α β (eqtoidₒ ua fe α β e) = e η β e = ≃ₒ-is-prop-valued fe α β (idtoeqₒ α β (eqtoidₒ ua fe α β e)) e the-type-of-ordinals-is-a-set : is-univalent 𝓤 → Fun-Ext → is-set (Ordinal 𝓤) the-type-of-ordinals-is-a-set ua fe {α} {β} = equiv-to-prop (idtoeqₒ α β , UAₒ ua fe α β) (≃ₒ-is-prop-valued fe α β) UAₒ-≃ : is-univalent 𝓤 → Fun-Ext → (α β : Ordinal 𝓤) → (α = β) ≃ (α ≃ₒ β) UAₒ-≃ ua fe α β = idtoeqₒ α β , UAₒ ua fe α β the-type-of-ordinals-is-locally-small : is-univalent 𝓤 → Fun-Ext → is-locally-small (Ordinal 𝓤) the-type-of-ordinals-is-locally-small ua fe α β = (α ≃ₒ β) , ≃-sym (UAₒ-≃ ua fe α β) \end{code} One of the many applications of the univalence axiom is to manufacture examples of types that are not sets. Here we have instead used it to prove that a certain type is a set. But see below for a proof that uses a weaker assumption. \begin{code} order-equivs-preserve-largest : (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (f : ⟨ α ⟩ → ⟨ β ⟩) → is-order-equiv α β f → (x : ⟨ α ⟩) → is-largest α x → is-largest β (f x) order-equivs-preserve-largest α β f (o , e , p) x ℓ = δ where f⁻¹ : ⟨ β ⟩ → ⟨ α ⟩ f⁻¹ = inverse f e δ : (y : ⟨ β ⟩) → y ≼⟨ β ⟩ f x δ y t l = IV where I : f⁻¹ t ≺⟨ α ⟩ f⁻¹ y I = p t y l II : f⁻¹ t ≺⟨ α ⟩ x II = ℓ (f⁻¹ y) (f⁻¹ t) I III : f (f⁻¹ t) ≺⟨ β ⟩ f x III = o (f⁻¹ t) x II IV : t ≺⟨ β ⟩ f x IV = transport (λ - → - ≺⟨ β ⟩ f x) (inverses-are-sections f e t) III \end{code} Added 25th Feb 2023. Alternative definition of ordinal equivalence \begin{code} _≃ₐ_ : Ordinal 𝓤 → Ordinal 𝓥 → 𝓤 ⊔ 𝓥 ̇ α ≃ₐ β = Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-equiv f × ((x x' : ⟨ α ⟩) → x ≺⟨ α ⟩ x' ↔ f x ≺⟨ β ⟩ f x') ≃ₐ-coincides-with-≃ₒ : FunExt → (α : Ordinal 𝓤) (β : Ordinal 𝓥) → (α ≃ₐ β) ≃ (α ≃ₒ β) ≃ₐ-coincides-with-≃ₒ fe α β = (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-equiv f × ((x x' : ⟨ α ⟩) → x ≺⟨ α ⟩ x' ↔ f x ≺⟨ β ⟩ f x')) ≃⟨ I ⟩ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , is-equiv f × (is-order-preserving α β f) × (is-order-reflecting α β f)) ≃⟨ II ⟩ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , (Σ e ꞉ is-equiv f , (is-order-preserving α β f) × (is-order-preserving β α (inv f e)))) ≃⟨ III ⟩ (Σ f ꞉ (⟨ α ⟩ → ⟨ β ⟩) , (is-order-preserving α β f) × (Σ e ꞉ is-equiv f , (is-order-preserving β α (inv f e)))) ■ where inv = inverse I = Σ-cong (λ f → ×-cong (≃-refl _) Π×-distr₂) II = Σ-cong (λ f → Σ-cong (λ e → ×-cong (≃-refl _) (b f e))) where b = λ f e → logically-equivalent-props-are-equivalent (being-order-reflecting-is-prop (λ {𝓤} {𝓥} → fe 𝓤 𝓥) α β f) (being-order-preserving-is-prop (λ {𝓤} {𝓥} → fe 𝓤 𝓥) β α (inv f e)) (order-reflecting-gives-inverse-order-preserving α β f e) (inverse-order-reflecting-gives-order-preserving α β f e) III = Σ-cong (λ f → Σ-flip) \end{code} If we only assume preunivalence, meaning that idtoeq is an embedding (rather than an equivalence), which is implied by each of univalence and the K axiom, we get that idtoeqₒ is an embedding (rather than an equivalence). This was suggested to me by Peter Lumsdaine in August 2022. \begin{code} idtoeqₒ-embedding : is-preunivalent 𝓤 → FunExt → (α β : Ordinal 𝓤) → (α = β) ↪ (α ≃ₒ β) idtoeqₒ-embedding {𝓤} pua fe α β = II where open relational-space {𝓤} {𝓤} {𝓤} (λ (X : 𝓤 ̇ ) (_<_ : X → X → 𝓤 ̇ ) → is-well-order _<_) (λ (X : 𝓤 ̇ ) (_<_ : X → X → 𝓤 ̇ ) → being-well-order-is-prop _<_ fe) (λ {X R} w {x} {y} → prop-valuedness R w x y) I : (α = β) ↪ (α ≅₂ β) I = M-embedding₂-bis pua pua (λ {𝓤} {𝓥} → fe 𝓤 𝓥) α β II : (α = β) ↪ (α ≃ₒ β) II = ≃-gives-↪ (≃ₐ-coincides-with-≃ₒ fe α β) ∘↪ I Ordinal-is-set-under-preunivalence : is-preunivalent 𝓤 → FunExt → is-set (Ordinal 𝓤) Ordinal-is-set-under-preunivalence {𝓤} pua fe {α} {β} = subtypes-of-props-are-props ⌊ idtoeqₒ-embedding pua fe α β ⌋ ⌊ idtoeqₒ-embedding pua fe α β ⌋-is-embedding (≃ₒ-is-prop-valued (fe _ _) α β) \end{code} NB. The above idtoeqₒ-embedding is constructed by a non-trivial procedure using preunivalence and function extensionality as assumptions, and so we may wonder whether it really is idtoeqₒ. It isn't on the nose, but it is pointwise equal to it on the nose: \begin{code} idtoeqₒ-embedding-really-is-idtoeqₒ : (pua : is-preunivalent 𝓤) (fe : FunExt) (α β : Ordinal 𝓤) → ⌊ idtoeqₒ-embedding pua fe α β ⌋ ∼ idtoeqₒ α β idtoeqₒ-embedding-really-is-idtoeqₒ pua fe α β refl = refl \end{code} And so equal: \begin{code} idtoeqₒ-embedding-really-is-idtoeqₒ' : (pua : is-preunivalent 𝓤) (fe : FunExt) (α β : Ordinal 𝓤) → ⌊ idtoeqₒ-embedding pua fe α β ⌋ = idtoeqₒ α β idtoeqₒ-embedding-really-is-idtoeqₒ' pua fe α β = dfunext (fe _ _) (idtoeqₒ-embedding-really-is-idtoeqₒ pua fe α β) \end{code}