MultiplicationProperties
Fredrik Nordvall Forsberg, 13 November 2023. In collaboration with Tom de Jong, Nicolai Kraus and Chuangjie Xu. Minor updates 9 and 11 September, 1 November 2024 and 15 July 2025. We prove several properties of ordinal multiplication, including that it preserves suprema of ordinals and that it enjoys a left-cancellation property.{-# OPTIONS --safe --without-K --lossy-unification #-} open import UF.Univalence module Ordinals.MultiplicationProperties (ua : Univalence) where open import UF.Base open import UF.Equiv open import UF.FunExt open import UF.Subsingletons open import UF.Subsingletons-FunExt open import UF.UA-FunExt open import UF.ClassicalLogic private fe : FunExt fe = Univalence-gives-FunExt ua fe' : Fun-Ext fe' {𝓤} {𝓥} = fe 𝓤 𝓥 open import MLTT.Spartan open import MLTT.Plus-Properties open import Ordinals.AdditionProperties ua open import Ordinals.Arithmetic fe open import Ordinals.Equivalence open import Ordinals.Exponentiation.TrichotomousLeastElement ua open import Ordinals.Maps open import Ordinals.OrdinalOfOrdinals ua open import Ordinals.Propositions ua open import Ordinals.Type open import Ordinals.Underlying ×ₒ-𝟘ₒ-right : (α : Ordinal 𝓤) → α ×ₒ 𝟘ₒ {𝓥} ＝ 𝟘ₒ ×ₒ-𝟘ₒ-right α = ⊴-antisym _ _ (to-⊴ (α ×ₒ 𝟘ₒ) 𝟘ₒ (λ (a , b) → 𝟘-elim b)) (𝟘ₒ-least-⊴ (α ×ₒ 𝟘ₒ)) ×ₒ-𝟘ₒ-left : (α : Ordinal 𝓤) → 𝟘ₒ {𝓥} ×ₒ α ＝ 𝟘ₒ ×ₒ-𝟘ₒ-left α = ⊴-antisym _ _ (to-⊴ (𝟘ₒ ×ₒ α) 𝟘ₒ (λ (b , a) → 𝟘-elim b)) (𝟘ₒ-least-⊴ (𝟘ₒ ×ₒ α)) 𝟙ₒ-left-neutral-×ₒ : (α : Ordinal 𝓤) → 𝟙ₒ {𝓤} ×ₒ α ＝ α 𝟙ₒ-left-neutral-×ₒ {𝓤} α = eqtoidₒ (ua _) fe' _ _ (f , f-order-preserving , f-is-equiv , g-order-preserving) where f : 𝟙 × ⟨ α ⟩ → ⟨ α ⟩ f = pr₂ g : ⟨ α ⟩ → 𝟙 × ⟨ α ⟩ g = ( ⋆ ,_) f-order-preserving : is-order-preserving (𝟙ₒ {𝓤} ×ₒ α) α f f-order-preserving x y (inl p) = p f-order-preserving x y (inr (e , q)) = 𝟘-elim q f-is-equiv : is-equiv f f-is-equiv = qinvs-are-equivs f (g , (λ _ → refl) , (λ _ → refl)) g-order-preserving : is-order-preserving α (𝟙ₒ {𝓤} ×ₒ α) g g-order-preserving x y p = inl p 𝟙ₒ-right-neutral-×ₒ : (α : Ordinal 𝓤) → α ×ₒ 𝟙ₒ {𝓤} ＝ α 𝟙ₒ-right-neutral-×ₒ {𝓤} α = eqtoidₒ (ua _) fe' _ _ (f , f-order-preserving , f-is-equiv , g-order-preserving) where f : ⟨ α ⟩ × 𝟙 → ⟨ α ⟩ f = pr₁ g : ⟨ α ⟩ → ⟨ α ⟩ × 𝟙 g = (_, ⋆ ) f-order-preserving : is-order-preserving (α ×ₒ 𝟙ₒ {𝓤}) α f f-order-preserving x y (inl p) = 𝟘-elim p f-order-preserving x y (inr (refl , p)) = p f-is-equiv : is-equiv f f-is-equiv = qinvs-are-equivs f (g , (λ _ → refl) , (λ _ → refl)) g-order-preserving : is-order-preserving α (α ×ₒ 𝟙ₒ {𝓤}) g g-order-preserving x y p = inr (refl , p)Because we use --lossy-unification to speed up typechecking we have to explicitly mention the universes in the lemma below; using them as variables (as usual) results in a unification error.×ₒ-assoc : {𝓤 𝓥 𝓦 : Universe} (α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦) → (α ×ₒ β) ×ₒ γ ＝ α ×ₒ (β ×ₒ γ) ×ₒ-assoc α β γ = eqtoidₒ (ua _) fe' ((α ×ₒ β) ×ₒ γ) (α ×ₒ (β ×ₒ γ)) (f , order-preserving-reflecting-equivs-are-order-equivs ((α ×ₒ β) ×ₒ γ) (α ×ₒ (β ×ₒ γ)) f f-equiv f-preserves-order f-reflects-order) where f : ⟨ (α ×ₒ β) ×ₒ γ ⟩ → ⟨ α ×ₒ (β ×ₒ γ) ⟩ f ((a , b) , c) = (a , (b , c)) g : ⟨ α ×ₒ (β ×ₒ γ) ⟩ → ⟨ (α ×ₒ β) ×ₒ γ ⟩ g (a , (b , c)) = ((a , b) , c) f-equiv : is-equiv f f-equiv = qinvs-are-equivs f (g , (λ x → refl) , (λ x → refl)) f-preserves-order : is-order-preserving ((α ×ₒ β) ×ₒ γ) (α ×ₒ (β ×ₒ γ)) f f-preserves-order _ _ (inl p) = inl (inl p) f-preserves-order _ _ (inr (r , inl p)) = inl (inr (r , p)) f-preserves-order _ _ (inr (r , inr (u , q))) = inr (to-×-＝ u r , q) f-reflects-order : is-order-reflecting ((α ×ₒ β) ×ₒ γ) (α ×ₒ (β ×ₒ γ)) f f-reflects-order _ _ (inl (inl p)) = inl p f-reflects-order _ _ (inl (inr (r , q))) = inr (r , (inl q)) f-reflects-order _ _ (inr (refl , q)) = inr (refl , (inr (refl , q)))The lemma below is as general as possible in terms of universe parameters because addition requires its arguments to come from the same universe, at least at present.×ₒ-distributes-+ₒ-right : (α : Ordinal 𝓤) (β γ : Ordinal 𝓥) → α ×ₒ (β +ₒ γ) ＝ (α ×ₒ β) +ₒ (α ×ₒ γ) ×ₒ-distributes-+ₒ-right α β γ = eqtoidₒ (ua _) fe' _ _ (f , f-order-preserving , f-is-equiv , g-order-preserving) where f : ⟨ α ×ₒ (β +ₒ γ) ⟩ → ⟨ (α ×ₒ β) +ₒ (α ×ₒ γ) ⟩ f (a , inl b) = inl (a , b) f (a , inr c) = inr (a , c) g : ⟨ (α ×ₒ β) +ₒ (α ×ₒ γ) ⟩ → ⟨ α ×ₒ (β +ₒ γ) ⟩ g (inl (a , b)) = a , inl b g (inr (a , c)) = a , inr c f-order-preserving : is-order-preserving _ _ f f-order-preserving (a , inl b) (a' , inl b') (inl p) = inl p f-order-preserving (a , inl b) (a' , inr c') (inl p) = ⋆ f-order-preserving (a , inr c) (a' , inr c') (inl p) = inl p f-order-preserving (a , inl b) (a' , inl .b) (inr (refl , q)) = inr (refl , q) f-order-preserving (a , inr c) (a' , inr .c) (inr (refl , q)) = inr (refl , q) f-order-preserving (a , inl b) (a' , inr c') (inr (e , q)) = 𝟘-elim (+disjoint e) f-order-preserving (a , inr c) (a' , inl b') (inl p) = 𝟘-elim p f-order-preserving (a , inr c) (a' , inl b') (inr (e , q)) = 𝟘-elim (+disjoint' e) f-is-equiv : is-equiv f f-is-equiv = qinvs-are-equivs f (g , η , ε) where η : g ∘ f ∼ id η (a , inl b) = refl η (a , inr c) = refl ε : f ∘ g ∼ id ε (inl (a , b)) = refl ε (inr (a , c)) = refl g-order-preserving : is-order-preserving _ _ g g-order-preserving (inl (a , b)) (inl (a' , b')) (inl p) = inl p g-order-preserving (inl (a , b)) (inl (a' , .b)) (inr (refl , q)) = inr (refl , q) g-order-preserving (inl (a , b)) (inr (a' , c')) p = inl ⋆ g-order-preserving (inr (a , c)) (inl b') p = 𝟘-elim p g-order-preserving (inr (a , c)) (inr (a' , c')) (inl p) = inl p g-order-preserving (inr (a , c)) (inr (a' , c')) (inr (refl , q)) = inr (refl , q)The following characterizes the initial segments of a product and is rather useful when working with simulations between products.×ₒ-↓ : (α β : Ordinal 𝓤) → {a : ⟨ α ⟩} {b : ⟨ β ⟩} → (α ×ₒ β) ↓ (a , b) ＝ (α ×ₒ (β ↓ b)) +ₒ (α ↓ a) ×ₒ-↓ α β {a} {b} = eqtoidₒ (ua _) fe' _ _ (f , f-order-preserving , f-is-equiv , g-order-preserving) where f : ⟨ (α ×ₒ β) ↓ (a , b) ⟩ → ⟨ (α ×ₒ (β ↓ b)) +ₒ (α ↓ a) ⟩ f ((x , y) , inl p) = inl (x , (y , p)) f ((x , y) , inr (r , q)) = inr (x , q) g : ⟨ (α ×ₒ (β ↓ b)) +ₒ (α ↓ a) ⟩ → ⟨ (α ×ₒ β) ↓ (a , b) ⟩ g (inl (x , y , p)) = (x , y) , inl p g (inr (x , q)) = (x , b) , inr (refl , q) f-order-preserving : is-order-preserving _ _ f f-order-preserving ((x , y) , inl p) ((x' , y') , inl p') (inl l) = inl l f-order-preserving ((x , y) , inl p) ((x' , _) , inl p') (inr (refl , l)) = inr ((ap (y ,_) (Prop-valuedness β _ _ p p')) , l) f-order-preserving ((x , y) , inl p) ((x' , y') , inr (r' , q')) l = ⋆ f-order-preserving ((x , y) , inr (refl , q)) ((x' , y') , inl p') (inl l) = 𝟘-elim (irrefl β y (Transitivity β _ _ _ l p')) f-order-preserving ((x , y) , inr (refl , q)) ((x' , _) , inl p') (inr (refl , l)) = 𝟘-elim (irrefl β y p') f-order-preserving ((x , y) , inr (refl , q)) ((x' , _) , inr (refl , q')) (inl l) = 𝟘-elim (irrefl β y l) f-order-preserving ((x , y) , inr (refl , q)) ((x' , _) , inr (refl , q')) (inr (_ , l)) = l f-is-equiv : is-equiv f f-is-equiv = qinvs-are-equivs f (g , η , ε) where η : g ∘ f ∼ id η ((x , y) , inl p) = refl η ((x , y) , inr (refl , q)) = refl ε : f ∘ g ∼ id ε (inl (x , y)) = refl ε (inr x) = refl g-order-preserving : is-order-preserving _ _ g g-order-preserving (inl (x , y , p)) (inl (x' , y' , p')) (inl l) = inl l g-order-preserving (inl (x , y , p)) (inl (x' , y' , p')) (inr (refl , l)) = inr (refl , l) g-order-preserving (inl (x , y , p)) (inr (x' , q')) _ = inl p g-order-preserving (inr (x , q)) (inl y') l = 𝟘-elim l g-order-preserving (inr (x , q)) (inr (x' , q')) l = inr (refl , l)We now prove several useful facts about (bounded) simulations between products.×ₒ-increasing-on-right : (α β γ : Ordinal 𝓤) → 𝟘ₒ ⊲ α → β ⊲ γ → (α ×ₒ β) ⊲ (α ×ₒ γ) ×ₒ-increasing-on-right α β γ (a , p) (c , q) = (a , c) , I where I = α ×ₒ β ＝⟨ 𝟘ₒ-right-neutral (α ×ₒ β) ⁻¹ ⟩ (α ×ₒ β) +ₒ 𝟘ₒ ＝⟨ ap₂ (λ -₁ -₂ → (α ×ₒ -₁) +ₒ -₂) q p ⟩ (α ×ₒ (γ ↓ c)) +ₒ (α ↓ a) ＝⟨ ×ₒ-↓ α γ ⁻¹ ⟩ (α ×ₒ γ) ↓ (a , c) ∎ ×ₒ-right-monotone-⊴ : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (γ : Ordinal 𝓦) → β ⊴ γ → (α ×ₒ β) ⊴ (α ×ₒ γ) ×ₒ-right-monotone-⊴ α β γ (g , sim-g) = f , f-initial-segment , f-order-preserving where f : ⟨ α ×ₒ β ⟩ → ⟨ α ×ₒ γ ⟩ f (a , b) = a , g b f-initial-segment : is-initial-segment (α ×ₒ β) (α ×ₒ γ) f f-initial-segment (a , b) (a' , c') (inl l) = (a' , b') , inl k , ap (a' ,_) q where I : Σ b' ꞉ ⟨ β ⟩ , b' ≺⟨ β ⟩ b × (g b' ＝ c') I = simulations-are-initial-segments β γ g sim-g b c' l b' = pr₁ I k = pr₁ (pr₂ I) q = pr₂ (pr₂ I) f-initial-segment (a , b) (a' , c') (inr (refl , q)) = (a' , b) , inr (refl , q) , refl f-order-preserving : is-order-preserving (α ×ₒ β) (α ×ₒ γ) f f-order-preserving (a , b) (a' , b') (inl p) = inl (simulations-are-order-preserving β γ g sim-g b b' p) f-order-preserving (a , b) (a' , b') (inr (refl , q)) = inr (refl , q) ×ₒ-≼-left : (α : Ordinal 𝓤) (β : Ordinal 𝓥) {a a' : ⟨ α ⟩} {b : ⟨ β ⟩} → a ≼⟨ α ⟩ a' → (a , b) ≼⟨ α ×ₒ β ⟩ (a' , b) ×ₒ-≼-left α β p (a₀ , b₀) (inl r) = inl r ×ₒ-≼-left α β p (a₀ , b₀) (inr (eq , r)) = inr (eq , p a₀ r)Multiplication satisfies the expected recursive equations (which classically define ordinal multiplication): zero is fixed by multiplication (this is ×ₒ-𝟘ₒ-right above), multiplication for successors is repeated addition and multiplication preserves suprema (i.e. it is continuous).×ₒ-successor : (α β : Ordinal 𝓤) → α ×ₒ (β +ₒ 𝟙ₒ) ＝ (α ×ₒ β) +ₒ α ×ₒ-successor α β = α ×ₒ (β +ₒ 𝟙ₒ) ＝⟨ ×ₒ-distributes-+ₒ-right α β 𝟙ₒ ⟩ ((α ×ₒ β) +ₒ (α ×ₒ 𝟙ₒ)) ＝⟨ ap ((α ×ₒ β) +ₒ_) (𝟙ₒ-right-neutral-×ₒ α) ⟩ (α ×ₒ β) +ₒ α ∎ open import UF.PropTrunc open import UF.Size module _ (pt : propositional-truncations-exist) (sr : Set-Replacement pt) where open import Ordinals.OrdinalOfOrdinalsSuprema ua open import Ordinals.SupremaPreservation ua pt sr open suprema pt sr open PropositionalTruncation pt ×ₒ-is-continuous : (α : Ordinal 𝓤) → is-continuous (α ×ₒ_) ×ₒ-is-continuous {𝓤} α {I} β = ⊴-antisym (α ×ₒ sup β) (sup (λ i → α ×ₒ β i)) ⦅1⦆ ⦅2⦆ where ⦅2⦆ : sup (λ i → α ×ₒ β i) ⊴ (α ×ₒ sup β) ⦅2⦆ = sup-is-lower-bound-of-upper-bounds (λ i → α ×ₒ β i) (α ×ₒ sup β) (λ i → ×ₒ-right-monotone-⊴ α (β i) (sup β) (sup-is-upper-bound β i)) ⦅1⦆ : (α ×ₒ sup β) ⊴ sup (λ i → α ×ₒ β i) ⦅1⦆ = ≼-gives-⊴ (α ×ₒ sup β) (sup (λ i → α ×ₒ β i)) ⦅1⦆-I where ⦅1⦆-I : (γ : Ordinal 𝓤) → γ ⊲ (α ×ₒ sup β) → γ ⊲ sup (λ i → α ×ₒ β i) ⦅1⦆-I _ ((a , y) , refl) = ⦅1⦆-III where ⦅1⦆-II : (Σ i ꞉ I , Σ b ꞉ ⟨ β i ⟩ , sup β ↓ y ＝ (β i) ↓ b) → ((α ×ₒ sup β) ↓ (a , y)) ⊲ sup (λ j → α ×ₒ β j) ⦅1⦆-II (i , b , e) = σ (a , b) , eq where σ : ⟨ α ×ₒ β i ⟩ → ⟨ sup (λ j → α ×ₒ β j) ⟩ σ = [ α ×ₒ β i , sup (λ j → α ×ₒ β j) ]⟨ sup-is-upper-bound _ i ⟩ eq = (α ×ₒ sup β) ↓ (a , y) ＝⟨ ×ₒ-↓ α (sup β) ⟩ (α ×ₒ (sup β ↓ y)) +ₒ (α ↓ a) ＝⟨ eq₁ ⟩ (α ×ₒ (β i ↓ b)) +ₒ (α ↓ a) ＝⟨ ×ₒ-↓ α (β i) ⁻¹ ⟩ (α ×ₒ β i) ↓ (a , b) ＝⟨ eq₂ ⟩ sup (λ j → α ×ₒ β j) ↓ σ (a , b) ∎ where eq₁ = ap (λ - → ((α ×ₒ -) +ₒ (α ↓ a))) e eq₂ = (initial-segment-of-sup-at-component (λ j → α ×ₒ β j) i (a , b)) ⁻¹ ⦅1⦆-III : ((α ×ₒ sup β) ↓ (a , y)) ⊲ sup (λ i → α ×ₒ β i) ⦅1⦆-III = ∥∥-rec (⊲-is-prop-valued _ _) ⦅1⦆-II (initial-segment-of-sup-is-initial-segment-of-some-component β y)In OperationsByCases, it is shown that the equations for successor and suprema uniquely specify the multiplication operation and lead to a definition by transfinite recursion. Added 17 September 2024 by Fredrik Nordvall Forsberg: Multiplication being monotone in the left argument is a constructive taboo. Addition 22 November 2024: monotonicity in the left argument is equivalent to Excluded Middle.×ₒ-minimal : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (a₀ : ⟨ α ⟩) (b₀ : ⟨ β ⟩) → is-least α a₀ → is-least β b₀ → is-minimal (α ×ₒ β) (a₀ , b₀) ×ₒ-minimal α β a₀ b₀ a₀-least b₀-least (a , b) (inl l) = irrefl β b (b₀-least b b l) ×ₒ-minimal α β a₀ b₀ a₀-least b₀-least (a , b) (inr (refl , l)) = irrefl α a (a₀-least a a l) ×ₒ-least : (α : Ordinal 𝓤) (β : Ordinal 𝓥) (a₀ : ⟨ α ⟩) (b₀ : ⟨ β ⟩) → is-least α a₀ → is-least β b₀ → is-least (α ×ₒ β) (a₀ , b₀) ×ₒ-least α β a₀ b₀ a₀-least b₀-least = minimal-is-least (α ×ₒ β) (a₀ , b₀) (×ₒ-minimal α β a₀ b₀ a₀-least b₀-least) ×ₒ-left-monotonicity-implies-EM : ((α β : Ordinal 𝓤) (γ : Ordinal 𝓥) → α ⊴ β → α ×ₒ γ ⊴ β ×ₒ γ) → EM 𝓤 ×ₒ-left-monotonicity-implies-EM hyp P isprop-P = III (f (⋆ , inr ⋆)) refl where α = 𝟙ₒ Pₒ = prop-ordinal P isprop-P β = 𝟙ₒ +ₒ Pₒ γ = 𝟚ₒ I : α ⊴ β I = ≼-gives-⊴ α β (transport (_≼ β) (𝟘ₒ-right-neutral 𝟙ₒ) (+ₒ-right-monotone 𝟙ₒ 𝟘ₒ Pₒ (𝟘ₒ-least Pₒ))) II : (α ×ₒ γ) ⊴ (β ×ₒ γ) II = hyp α β γ I f = pr₁ II f-sim = pr₂ II f-preserves-least : f (⋆ , inl ⋆) ＝ (inl ⋆ , inl ⋆) f-preserves-least = simulations-preserve-least (α ×ₒ γ) (β ×ₒ γ) (⋆ , inl ⋆) (inl ⋆ , inl ⋆) f f-sim (×ₒ-least α γ ⋆ (inl ⋆) ⋆-least (left-preserves-least 𝟙ₒ 𝟙ₒ ⋆ ⋆-least)) (×ₒ-least β γ (inl ⋆) (inl ⋆) (left-preserves-least 𝟙ₒ Pₒ ⋆ ⋆-least) (left-preserves-least 𝟙ₒ 𝟙ₒ ⋆ ⋆-least)) where ⋆-least : is-least (𝟙ₒ {𝓤}) ⋆ ⋆-least ⋆ ⋆ = 𝟘-elim III : (x : ⟨ β ×ₒ γ ⟩) → f (⋆ , inr ⋆) ＝ x → P + ¬ P III (inl ⋆ , inl ⋆) r = 𝟘-elim (+disjoint' III₂) where III₁ = f (⋆ , inr ⋆) ＝⟨ r ⟩ (inl ⋆ , inl ⋆) ＝⟨ f-preserves-least ⁻¹ ⟩ f (⋆ , inl ⋆) ∎ III₂ : inr ⋆ ＝ inl ⋆ III₂ = ap pr₂ (simulations-are-lc _ _ f f-sim III₁) III (inl ⋆ , inr ⋆) r = inr (λ p → 𝟘-elim (+disjoint (III₆ p))) where III₃ : (p : P) → Σ x ꞉ ⟨ 𝟙ₒ ×ₒ 𝟚ₒ ⟩ , (x ≺⟨ 𝟙ₒ ×ₒ 𝟚ₒ ⟩ (⋆ , inr ⋆)) × (f x ＝ (inr p , inl ⋆)) III₃ p = simulations-are-initial-segments (α ×ₒ γ) (β ×ₒ γ) f f-sim (⋆ , inr ⋆) (inr p , inl ⋆) (transport⁻¹ (λ - → (inr p , inl ⋆) ≺⟨ β ×ₒ γ ⟩ - ) r (inl ⋆)) III₄ : (p : P) → Σ x ꞉ ⟨ 𝟙ₒ ×ₒ 𝟚ₒ ⟩ , (x ≺⟨ 𝟙ₒ ×ₒ 𝟚ₒ ⟩ (⋆ , inr ⋆)) × (f x ＝ (inr p , inl ⋆)) → f (⋆ , inl ⋆) ＝ (inr p , inl ⋆) III₄ p ((⋆ , inl ⋆) , l , q) = q III₄ p ((⋆ , inr ⋆) , l , q) = 𝟘-elim (irrefl (𝟙ₒ ×ₒ 𝟚ₒ) (⋆ , inr ⋆) l) III₅ : (p : P) → (inl ⋆ , inl ⋆) ＝ (inr p , inl ⋆) III₅ p = (inl ⋆ , inl ⋆) ＝⟨ f-preserves-least ⁻¹ ⟩ f (⋆ , inl ⋆) ＝⟨ III₄ p (III₃ p) ⟩ (inr p , inl ⋆) ∎ III₆ : (p : P) → inl ⋆ ＝ inr p III₆ p = ap pr₁ (III₅ p) III (inr p , c) r = inl p EM-implies-×ₒ-left-monotonicity : EM (𝓤 ⊔ 𝓥) → (α β : Ordinal 𝓤) (γ : Ordinal 𝓥) → α ⊴ β → (α ×ₒ γ) ⊴ (β ×ₒ γ) EM-implies-×ₒ-left-monotonicity em α β γ (g , g-sim) = ≼-gives-⊴ (α ×ₒ γ) (β ×ₒ γ) (EM-implies-order-preserving-gives-≼ em (α ×ₒ γ) (β ×ₒ γ) (f , f-order-preserving)) where f : ⟨ α ×ₒ γ ⟩ → ⟨ β ×ₒ γ ⟩ f (a , c) = (g a , c) f-order-preserving : is-order-preserving (α ×ₒ γ) (β ×ₒ γ) f f-order-preserving (a , c) (a' , c') (inl l) = inl l f-order-preserving (a , c) (a' , c) (inr (refl , l)) = inr (refl , simulations-are-order-preserving α β g g-sim a a' l) EM-implies-induced-⊴-on-×ₒ : EM 𝓤 → (α β γ δ : Ordinal 𝓤) → α ⊴ γ → β ⊴ δ → (α ×ₒ β) ⊴ (γ ×ₒ δ) EM-implies-induced-⊴-on-×ₒ em α β γ δ 𝕗 𝕘 = ⊴-trans (α ×ₒ β) (α ×ₒ δ) (γ ×ₒ δ) (×ₒ-right-monotone-⊴ α β δ 𝕘) (EM-implies-×ₒ-left-monotonicity em α γ δ 𝕗)To prove that multiplication is left cancellable, we require the following technical lemma: if α > 𝟘, then every simulation from α ×ₒ β to α ×ₒ γ + α ↓ a₁ firstly never hits the second summand, and secondly, in the first component, it decomposes as the identity on the first component and a function β → γ on the second component, viz. one that is independent of the first component. The inspiration for this lemma is the lemma simulation-product-decomposition below, which only deals with simulations f : α ×ₒ β ⊴ α ×ₒ γ (ie, with α ↓ a₁ = 𝟘ₒ in the context of the current lemma). However the more general statement seems to be necessary for proving left cancellability with respect to ⊴, rather than just with respect to ＝.simulation-product-decomposition-generalized : (α : Ordinal 𝓤) → 𝟘ₒ ⊲ α → (β γ : Ordinal 𝓤) → (a₁ : ⟨ α ⟩) → ((f , _) : α ×ₒ β ⊴ α ×ₒ γ +ₒ (α ↓ a₁)) → Σ g ꞉ (⟨ β ⟩ → ⟨ γ ⟩) , ((a : ⟨ α ⟩) (b : ⟨ β ⟩) → f (a , b) ＝ inl (a , g b)) simulation-product-decomposition-generalized {𝓤} α (a₀ , a₀-least) = II where P : Ordinal 𝓤 → 𝓤 ⁺ ̇ P β = (γ : Ordinal 𝓤) (a₁ : ⟨ α ⟩) ((f , _) : α ×ₒ β ⊴ α ×ₒ γ +ₒ (α ↓ a₁)) → (b : ⟨ β ⟩) → Σ c ꞉ ⟨ γ ⟩ , ((a : ⟨ α ⟩) → f (a , b) ＝ inl (a , c)) P₀ : Ordinal 𝓤 → 𝓤 ⁺ ̇ P₀ β = (a₁ : ⟨ α ⟩) (γ : Ordinal 𝓤) ((f , _) : α ×ₒ β ⊴ α ×ₒ γ +ₒ (α ↓ a₁)) (b : ⟨ β ⟩) (x : ⟨ (α ×ₒ γ) +ₒ (α ↓ a₁) ⟩) → f (a₀ , b) ＝ x → Σ c ꞉ ⟨ γ ⟩ , f (a₀ , b) ＝ inl (a₀ , c) I : (β γ : Ordinal 𝓤) (a₁ : ⟨ α ⟩) ((f , _) : α ×ₒ β ⊴ (α ×ₒ γ) +ₒ (α ↓ a₁)) (b : ⟨ β ⟩) → α ×ₒ (β ↓ b) ＝ α ×ₒ γ +ₒ (α ↓ a₁) ↓ f (a₀ , b) I β γ a₁ 𝕗@(f , f-sim) b = α ×ₒ (β ↓ b) ＝⟨ I₁ ⟩ α ×ₒ (β ↓ b) +ₒ (α ↓ a₀) ＝⟨ ×ₒ-↓ α β ⁻¹ ⟩ α ×ₒ β ↓ (a₀ , b) ＝⟨ I₂ ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ f (a₀ , b) ∎ where I₁ = 𝟘ₒ-right-neutral (α ×ₒ (β ↓ b)) ⁻¹ ∙ ap (α ×ₒ (β ↓ b) +ₒ_) a₀-least I₂ = simulations-preserve-↓ _ _ 𝕗 (a₀ , b) 𝕘₁ : (β : Ordinal 𝓤) → ((b : ⟨ β ⟩) → P (β ↓ b)) → P₀ β 𝕘₁ β IH a₁ γ 𝕗@(f , _) b (inl (a' , c)) e = c , III where eq = α ×ₒ (β ↓ b) ＝⟨ I β γ a₁ 𝕗 b ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ f (a₀ , b) ＝⟨ ap ((α ×ₒ γ +ₒ (α ↓ a₁)) ↓_) e ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ inl (a' , c) ＝⟨ +ₒ-↓-left (a' , c) ⁻¹ ⟩ α ×ₒ γ ↓ (a' , c) ＝⟨ ×ₒ-↓ α γ ⟩ α ×ₒ (γ ↓ c) +ₒ (α ↓ a') ∎ 𝕗' : α ×ₒ (β ↓ b) ⊴ α ×ₒ (γ ↓ c) +ₒ (α ↓ a') f' = Idtofunₒ eq 𝕗' = f' , Idtofunₒ-is-simulation eq 𝕗'⁻¹ : α ×ₒ (γ ↓ c) +ₒ (α ↓ a') ⊴ α ×ₒ (β ↓ b) f'⁻¹ = Idtofunₒ (eq ⁻¹) 𝕗'⁻¹ = f'⁻¹ , Idtofunₒ-is-simulation (eq ⁻¹) II : a' ＝ a₀ II = Extensionality α a' a₀ (λ x l → 𝟘-elim (II₁ x l)) (λ x l → 𝟘-elim (transport⁻¹ ⟨_⟩ a₀-least (x , l))) where II₁ : (x : ⟨ α ⟩) → ¬ (x ≺⟨ α ⟩ a') II₁ x l = +disjoint II₂ where y : ⟨ α ×ₒ (β ↓ b) ⟩ y = f'⁻¹ (inr (x , l)) y₁ = pr₁ y y₂ = pr₂ y z : ⟨ γ ↓ c ⟩ z = pr₁ (IH b (γ ↓ c) a' 𝕗' y₂) II₂ = inl (y₁ , z) ＝⟨ pr₂ (IH b (γ ↓ c) a' 𝕗' y₂) y₁ ⁻¹ ⟩ f' (f'⁻¹ (inr (x , l))) ＝⟨ Idtofunₒ-retraction eq (inr (x , l)) ⟩ inr (x , l) ∎ III = f (a₀ , b) ＝⟨ e ⟩ inl (a' , c) ＝⟨ ap (λ - → inl (- , c)) II ⟩ inl (a₀ , c) ∎ 𝕘₁ β _ a₁ γ 𝕗@(f , f-sim) b (inr (x , p)) e = 𝟘-elim (ν (a₁ , refl)) where eq-I = α ×ₒ (β ↓ b) ＝⟨ I β γ a₁ 𝕗 b ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ f (a₀ , b) ＝⟨ ap ((α ×ₒ γ +ₒ (α ↓ a₁)) ↓_) e ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ inr (x , p) ＝⟨ +ₒ-↓-right (x , p) ⁻¹ ⟩ α ×ₒ γ +ₒ (α ↓ a₁ ↓ (x , p)) ＝⟨ eq-I₁ ⟩ α ×ₒ γ +ₒ (α ↓ x) ∎ where eq-I₁ = ap ((α ×ₒ γ) +ₒ_) (iterated-↓ α a₁ x p) eq-II = α ×ₒ γ +ₒ ((α ↓ x) +ₒ α) ＝⟨ +ₒ-assoc (α ×ₒ γ) (α ↓ x) α ⁻¹ ⟩ α ×ₒ γ +ₒ (α ↓ x) +ₒ α ＝⟨ ap (_+ₒ α) eq-I ⁻¹ ⟩ α ×ₒ (β ↓ b) +ₒ α ＝⟨ ×ₒ-successor α (β ↓ b) ⁻¹ ⟩ α ×ₒ ((β ↓ b) +ₒ 𝟙ₒ) ∎ ineq-I : α ×ₒ γ +ₒ ((α ↓ x) +ₒ α) ⊴ α ×ₒ γ +ₒ (α ↓ a₁) ineq-I = transport⁻¹ (λ - → - ⊴ α ×ₒ γ +ₒ (α ↓ a₁)) eq-II (⊴-trans (α ×ₒ ((β ↓ b) +ₒ 𝟙ₒ)) (α ×ₒ β) (α ×ₒ γ +ₒ (α ↓ a₁)) (×ₒ-right-monotone-⊴ α ((β ↓ b) +ₒ 𝟙ₒ) β (upper-bound-of-successors-of-initial-segments β b)) 𝕗) ineq-II : (α ↓ x) +ₒ α ⊴ α ↓ a₁ ineq-II = +ₒ-left-reflects-⊴ (α ×ₒ γ) ((α ↓ x) +ₒ α) (α ↓ a₁) ineq-I h : ⟨ α ⟩ → ⟨ α ↓ a₁ ⟩ h a = [ (α ↓ x) +ₒ α , α ↓ a₁ ]⟨ ineq-II ⟩ (inr a) h-order-preserving : is-order-preserving α (α ↓ a₁) h h-order-preserving a a' l = simulations-are-order-preserving ((α ↓ x) +ₒ α) (α ↓ a₁) [ (α ↓ x) +ₒ α , α ↓ a₁ ]⟨ ineq-II ⟩ ([ (α ↓ x) +ₒ α , α ↓ a₁ ]⟨ ineq-II ⟩-is-simulation) (inr a) (inr a') l ν : ¬ (α ↓ a₁ ⊲ α) ν = order-preserving-gives-not-⊲ α (α ↓ a₁) (h , h-order-preserving) 𝕘₂ : (β : Ordinal 𝓤) → ((b : ⟨ β ⟩) → P (β ↓ b)) → P β 𝕘₂ β IH γ a₁ 𝕗@(f , f-sim) b = c , c-satisfies-equation where c : ⟨ γ ⟩ c = pr₁ (𝕘₁ β IH a₁ γ 𝕗 b (f (a₀ , b)) refl) c-spec : f (a₀ , b) ＝ inl (a₀ , c) c-spec = pr₂ (𝕘₁ β IH a₁ γ 𝕗 b (f (a₀ , b)) refl) c-satisfies-equation : (a : ⟨ α ⟩) → f (a , b) ＝ inl (a , c) c-satisfies-equation a = ↓-lc (α ×ₒ γ +ₒ (α ↓ a₁)) _ _ eq-II where eq-I = α ×ₒ (β ↓ b) ＝⟨ I β γ a₁ 𝕗 b ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ f (a₀ , b) ＝⟨ eq-I₁ ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ inl (a₀ , c) ＝⟨ +ₒ-↓-left (a₀ , c) ⁻¹ ⟩ α ×ₒ γ ↓ (a₀ , c) ＝⟨ ×ₒ-↓ α γ ⟩ α ×ₒ (γ ↓ c) +ₒ (α ↓ a₀) ＝⟨ eq-I₂ ⟩ α ×ₒ (γ ↓ c) ∎ where eq-I₁ = ap (((α ×ₒ γ) +ₒ (α ↓ a₁)) ↓_) c-spec eq-I₂ = ap ((α ×ₒ (γ ↓ c)) +ₒ_) a₀-least ⁻¹ ∙ 𝟘ₒ-right-neutral (α ×ₒ (γ ↓ c)) eq-II = α ×ₒ γ +ₒ (α ↓ a₁) ↓ f (a , b) ＝⟨ eq-II₁ ⟩ α ×ₒ β ↓ (a , b) ＝⟨ ×ₒ-↓ α β ⟩ α ×ₒ (β ↓ b) +ₒ (α ↓ a) ＝⟨ ap (_+ₒ (α ↓ a)) eq-I ⟩ α ×ₒ (γ ↓ c) +ₒ (α ↓ a) ＝⟨ ×ₒ-↓ α γ ⁻¹ ⟩ α ×ₒ γ ↓ (a , c) ＝⟨ +ₒ-↓-left (a , c) ⟩ α ×ₒ γ +ₒ (α ↓ a₁) ↓ inl (a , c) ∎ where eq-II₁ = (simulations-preserve-↓ _ _ 𝕗 (a , b)) ⁻¹ 𝕘 : (β : Ordinal 𝓤) → P β 𝕘 = transfinite-induction-on-OO P 𝕘₂ II : (β γ : Ordinal 𝓤) → (a₁ : ⟨ α ⟩) → ((f , _) : α ×ₒ β ⊴ α ×ₒ γ +ₒ (α ↓ a₁)) → Σ g ꞉ (⟨ β ⟩ → ⟨ γ ⟩) , ((a : ⟨ α ⟩) (b : ⟨ β ⟩) → f (a , b) ＝ inl (a , g b)) II β γ a₁ 𝕗 = (λ b → pr₁ (𝕘 β γ a₁ 𝕗 b)) , (λ a b → pr₂ (𝕘 β γ a₁ 𝕗 b) a) ×ₒ-left-cancellable-⊴-generalized : (α β γ : Ordinal 𝓤) (a₁ : ⟨ α ⟩) → 𝟘ₒ ⊲ α → α ×ₒ β ⊴ (α ×ₒ γ) +ₒ (α ↓ a₁) → β ⊴ γ ×ₒ-left-cancellable-⊴-generalized α β γ a₁ p@(a₀ , a₀-least) 𝕗@(f , f-sim) = (g , g-is-initial-segment , g-is-order-preserving) where g : ⟨ β ⟩ → ⟨ γ ⟩ g = pr₁ (simulation-product-decomposition-generalized α p β γ a₁ 𝕗) g-property : (a : ⟨ α ⟩) (b : ⟨ β ⟩) → f (a , b) ＝ inl (a , g b) g-property = pr₂ (simulation-product-decomposition-generalized α p β γ a₁ 𝕗) g-is-order-preserving : is-order-preserving β γ g g-is-order-preserving b b' l = III II where I : f (a₀ , b) ≺⟨ (α ×ₒ γ) +ₒ (α ↓ a₁) ⟩ f (a₀ , b') I = simulations-are-order-preserving _ _ f f-sim (a₀ , b) (a₀ , b') (inl l) II : inl (a₀ , g b) ≺⟨ (α ×ₒ γ) +ₒ (α ↓ a₁) ⟩ inl (a₀ , g b') II = transport₂ (λ x y → x ≺⟨ ((α ×ₒ γ) +ₒ (α ↓ a₁))⟩ y) (g-property a₀ b) (g-property a₀ b') I III : (a₀ , g b) ≺⟨ (α ×ₒ γ) ⟩ (a₀ , g b') → g b ≺⟨ γ ⟩ g b' III (inl p) = p III (inr (r , q)) = 𝟘-elim (irrefl α a₀ q) g-is-initial-segment : is-initial-segment β γ g g-is-initial-segment b c l = b' , II k , III where l₁ : inl (a₀ , c) ≺⟨ (α ×ₒ γ) +ₒ (α ↓ a₁) ⟩ inl (a₀ , g b) l₁ = inl l l₂ : inl (a₀ , c) ≺⟨ (α ×ₒ γ) +ₒ (α ↓ a₁) ⟩ f (a₀ , b) l₂ = transport⁻¹ (λ - → inl (a₀ , c) ≺⟨ ((α ×ₒ γ) +ₒ (α ↓ a₁))⟩ -) (g-property a₀ b) l₁ σ : Σ y ꞉ ⟨ α ×ₒ β ⟩ , (y ≺⟨ α ×ₒ β ⟩ (a₀ , b)) × (f y ＝ (inl (a₀ , c))) σ = simulations-are-initial-segments _ _ f f-sim (a₀ , b) (inl (a₀ , c)) l₂ a' = pr₁ (pr₁ σ) b' = pr₂ (pr₁ σ) k = pr₁ (pr₂ σ) e = pr₂ (pr₂ σ) II : (a' , b') ≺⟨ α ×ₒ β ⟩ (a₀ , b) → b' ≺⟨ β ⟩ b II (inl p) = p II (inr (r , q)) = 𝟘-elim (Idtofunₒ (a₀-least ⁻¹) (a' , q)) III : g b' ＝ c III = ap pr₂ (inl-lc (inl (a' , g b') ＝⟨ g-property a' b' ⁻¹ ⟩ f (a' , b') ＝⟨ e ⟩ inl (a₀ , c) ∎)) ×ₒ-left-cancellable-⊴ : (α β γ : Ordinal 𝓤) → 𝟘ₒ ⊲ α → (α ×ₒ β) ⊴ (α ×ₒ γ) → β ⊴ γ ×ₒ-left-cancellable-⊴ α β γ p@(a₀ , a₀-least) 𝕗 = ×ₒ-left-cancellable-⊴-generalized α β γ a₀ p (transport (α ×ₒ β ⊴_) (α ×ₒ γ ＝⟨ 𝟘ₒ-right-neutral (α ×ₒ γ) ⁻¹ ⟩ α ×ₒ γ +ₒ 𝟘ₒ ＝⟨ ap ((α ×ₒ γ) +ₒ_) a₀-least ⟩ α ×ₒ γ +ₒ (α ↓ a₀) ∎) 𝕗)The following result states that multiplication for ordinals can be cancelled on the left. Interestingly, Andrew Swan [Swa18] proved that the corresponding result for sets is not provable constructively already for α = 𝟚: there are toposes where the statement 𝟚 × X ≃ 𝟚 × Y → X ≃ Y is not true for certain objects X and Y in the topos. [Swa18] Andrew Swan. On Dividing by Two in Constructive Mathematics 2018. https://arxiv.org/abs/1804.04490×ₒ-left-cancellable : (α β γ : Ordinal 𝓤) → 𝟘ₒ ⊲ α → (α ×ₒ β) ＝ (α ×ₒ γ) → β ＝ γ ×ₒ-left-cancellable {𝓤 = 𝓤} α β γ p e = ⊴-antisym β γ (f β γ e) (f γ β (e ⁻¹)) where f : (β γ : Ordinal 𝓤) → (α ×ₒ β) ＝ (α ×ₒ γ) → β ⊴ γ f β γ e = ×ₒ-left-cancellable-⊴ α β γ p (≃ₒ-to-⊴ (α ×ₒ β) (α ×ₒ γ) (idtoeqₒ (α ×ₒ β) (α ×ₒ γ) e))As mentioned above, the generalized decomposition lemma for simulation from a product was inspired by the following less general lemma for which we give both an indirect and a direct proof (with more general universe levels).simulation-product-decomposition' : (α β γ : Ordinal 𝓤) ((a₀ , a₀-least) : 𝟘ₒ ⊲ α) ((f , _) : (α ×ₒ β) ⊴ (α ×ₒ γ)) (a : ⟨ α ⟩) (b : ⟨ β ⟩) → f (a , b) ＝ (a , pr₂ (f (a₀ , b))) simulation-product-decomposition' α β γ (a₀ , a₀-least) 𝕗@(f , f-sim) a = III where 𝕗' : α ×ₒ β ⊴ α ×ₒ γ +ₒ (α ↓ a) 𝕗' = ⊴-trans (α ×ₒ β) (α ×ₒ γ) (α ×ₒ γ +ₒ (α ↓ a)) 𝕗 (+ₒ-left-⊴ (α ×ₒ γ) (α ↓ a)) f' = [ α ×ₒ β , α ×ₒ γ +ₒ (α ↓ a) ]⟨ 𝕗' ⟩ I : Σ g ꞉ (⟨ β ⟩ → ⟨ γ ⟩) , ((a' : ⟨ α ⟩) (b : ⟨ β ⟩) → f' (a' , b) ＝ inl (a' , g b)) I = simulation-product-decomposition-generalized α (a₀ , a₀-least) β γ a 𝕗' g = pr₁ I g-property = pr₂ I II : (b : ⟨ β ⟩) → g b ＝ pr₂ (f (a₀ , b)) II b = ap pr₂ (inl-lc (inl (a₀ , g b) ＝⟨ (g-property a₀ b) ⁻¹ ⟩ f' (a₀ , b) ＝⟨refl⟩ inl (f (a₀ , b)) ∎)) III : (b : ⟨ β ⟩) → f (a , b) ＝ a , pr₂ (f (a₀ , b)) III b = inl-lc (inl (f (a , b)) ＝⟨ g-property a b ⟩ inl (a , g b) ＝⟨ ap (λ - → inl (a , -)) (II b) ⟩ inl (a , pr₂ (f (a₀ , b))) ∎) simulation-product-decomposition : (α : Ordinal 𝓤) (β γ : Ordinal 𝓥) ((a₀ , a₀-least) : 𝟘ₒ ⊲ α) ((f , _) : (α ×ₒ β) ⊴ (α ×ₒ γ)) → (a : ⟨ α ⟩) (b : ⟨ β ⟩) → f (a , b) ＝ (a , pr₂ (f (a₀ , b))) simulation-product-decomposition {𝓤} {𝓥} α β γ (a₀ , a₀-least) (f , sim@(init-seg , order-pres)) a b = I where f' : ⟨ α ×ₒ β ⟩ → ⟨ α ×ₒ γ ⟩ f' (a , b) = (a , pr₂ (f (a₀ , b))) P : ⟨ α ×ₒ β ⟩ → 𝓤 ⊔ 𝓥 ̇ P (a , b) = (f (a , b)) ＝ f' (a , b) I : P (a , b) I = Transfinite-induction (α ×ₒ β) P II (a , b) where II : (x : ⟨ α ×ₒ β ⟩) → ((y : ⟨ α ×ₒ β ⟩) → y ≺⟨ α ×ₒ β ⟩ x → P y) → P x II (a , b) IH = Extensionality (α ×ₒ γ) (f (a , b)) (f' (a , b)) III IV where III : (u : ⟨ α ×ₒ γ ⟩) → u ≺⟨ α ×ₒ γ ⟩ f (a , b) → u ≺⟨ α ×ₒ γ ⟩ f' (a , b) III (a' , c') p = transport (λ - → - ≺⟨ α ×ₒ γ ⟩ f' (a , b)) III₂ (III₃ p') where III₁ : Σ (a'' , b') ꞉ ⟨ α ×ₒ β ⟩ , (a'' , b') ≺⟨ α ×ₒ β ⟩ (a , b) × (f (a'' , b') ＝ a' , c') III₁ = init-seg (a , b) (a' , c') p a'' = pr₁ (pr₁ III₁) b' = pr₂ (pr₁ III₁) p' = pr₁ (pr₂ III₁) eq : f (a'' , b') ＝ (a' , c') eq = pr₂ (pr₂ III₁) III₂ : f' (a'' , b') ＝ (a' , c') III₂ = IH (a'' , b') p' ⁻¹ ∙ eq III₃ : (a'' , b') ≺⟨ α ×ₒ β ⟩ (a , b) → f' (a'' , b') ≺⟨ α ×ₒ γ ⟩ f' (a , b) III₃ (inl q) = h (order-pres (a₀' , b') (a₀ , b) (inl q)) where a₀' : ⟨ α ⟩ a₀' = pr₁ (f (a₀ , b)) ih : (f (a₀' , b')) ＝ f' (a₀' , b') ih = IH (a₀' , b') (inl q) h : f (a₀' , b') ≺⟨ α ×ₒ γ ⟩ f (a₀ , b) → f' (a'' , b') ≺⟨ α ×ₒ γ ⟩ f' (a , b) h (inl r) = inl (transport (λ - → - ≺⟨ γ ⟩ pr₂ (f (a₀ , b))) (ap pr₂ ih) r) h (inr (_ , r)) = 𝟘-elim (irrefl α a₀' (transport (λ - → - ≺⟨ α ⟩ a₀') (ap pr₁ ih) r)) III₃ (inr (e , q)) = inr (ap (λ - → pr₂ (f (a₀ , -))) e , q) IV : (u : ⟨ α ×ₒ γ ⟩) → u ≺⟨ α ×ₒ γ ⟩ f' (a , b) → u ≺⟨ α ×ₒ γ ⟩ f (a , b) IV (a' , c') (inl p) = l₂ (a' , c') (inl p) where l₁ : a₀ ≼⟨ α ⟩ a l₁ x p = 𝟘-elim (transport ⟨_⟩ (a₀-least ⁻¹) (x , p)) l₂ : f (a₀ , b) ≼⟨ α ×ₒ γ ⟩ f (a , b) l₂ = simulations-are-monotone _ _ f sim (a₀ , b) (a , b) (×ₒ-≼-left α β l₁) IV (a' , c') (inr (r , q)) = transport (λ - → - ≺⟨ α ×ₒ γ ⟩ f (a , b)) eq (order-pres (a' , b) (a , b) (inr (refl , q))) where eq = f (a' , b) ＝⟨ IH (a' , b) (inr (refl , q)) ⟩ f' (a' , b) ＝⟨refl⟩ (a' , pr₂ (f (a₀ , b))) ＝⟨ ap (a' ,_) (r ⁻¹) ⟩ (a' , c') ∎Using similar techniques, we can also prove that multiplication is left cancellable with respect to ⊲.simulation-product-decomposition-leftover-empty : (α β γ : Ordinal 𝓤) → 𝟘ₒ ⊲ α → (a : ⟨ α ⟩) → (α ×ₒ β) ＝ (α ×ₒ γ +ₒ (α ↓ a)) → (α ×ₒ β) ＝ (α ×ₒ γ) simulation-product-decomposition-leftover-empty α β γ (a₀ , p) a e = II where a-least : (x : ⟨ α ⟩) → ¬ (x ≺⟨ α ⟩ a) a-least x l = +disjoint (ν ⁻¹) where 𝕗 : α ×ₒ β ⊴ α ×ₒ γ +ₒ (α ↓ a) f = Idtofunₒ e 𝕗 = f , Idtofunₒ-is-simulation e 𝕗⁻¹ : α ×ₒ γ +ₒ (α ↓ a) ⊴ α ×ₒ β f⁻¹ = Idtofunₒ (e ⁻¹) 𝕗⁻¹ = f⁻¹ , Idtofunₒ-is-simulation (e ⁻¹) f-decomposition : Σ g ꞉ (⟨ β ⟩ → ⟨ γ ⟩) , ((a : ⟨ α ⟩) (b : ⟨ β ⟩) → f (a , b) ＝ inl (a , g b) ) f-decomposition = simulation-product-decomposition-generalized α (a₀ , p) β γ a 𝕗 g = pr₁ f-decomposition ν = (inr (x , l)) ＝⟨ (Idtofunₒ-retraction e (inr (x , l))) ⁻¹ ⟩ f (f⁻¹ (inr (x , l))) ＝⟨ pr₂ (f-decomposition) x' y' ⟩ inl (x' , g y') ∎ where x' = pr₁ (f⁻¹ (inr (x , l))) y' = pr₂ (f⁻¹ (inr (x , l))) I : a ＝ a₀ I = Extensionality α a a₀ (λ x l → 𝟘-elim (a-least x l)) (λ x l → 𝟘-elim (Idtofunₒ (p ⁻¹) (x , l))) II = α ×ₒ β ＝⟨ e ⟩ α ×ₒ γ +ₒ (α ↓ a) ＝⟨ ap ((α ×ₒ γ) +ₒ_) (ap (α ↓_) I ∙ p ⁻¹) ⟩ α ×ₒ γ +ₒ 𝟘ₒ ＝⟨ 𝟘ₒ-right-neutral (α ×ₒ γ) ⟩ α ×ₒ γ ∎ ×ₒ-left-cancellable-⊲ : (α β γ : Ordinal 𝓤) → 𝟘ₒ ⊲ α → α ×ₒ β ⊲ α ×ₒ γ → β ⊲ γ ×ₒ-left-cancellable-⊲ α β γ α-positive ((a , c) , p) = c , III where I : α ×ₒ β ＝ α ×ₒ (γ ↓ c) +ₒ (α ↓ a) I = p ∙ ×ₒ-↓ α γ II : α ×ₒ β ＝ α ×ₒ (γ ↓ c) II = simulation-product-decomposition-leftover-empty α β (γ ↓ c) α-positive a I III : β ＝ γ ↓ c III = ×ₒ-left-cancellable α β (γ ↓ c) α-positive IIAdded 15 July 2025 by Tom de Jong. Updated 6 October 2026 by Tom de Jong to reflect that we can even restrict to ordinals with a trichotomous least element.×ₒ-as-large-as-right-factor-implies-EM' : ((α β : Ordinal 𝓤) → has-trichotomous-least-element α → has-trichotomous-least-element β → 𝟘ₒ ⊲ α → β ⊴ α ×ₒ β) → EM 𝓤 ×ₒ-as-large-as-right-factor-implies-EM' hyp P P-is-prop = IV (f (inr ⋆)) refl where Pₒ = prop-ordinal P P-is-prop α = 𝟙ₒ +ₒ Pₒ β = 𝟚ₒ 𝕗 : β ⊴ α ×ₒ β 𝕗 = hyp α β (decomposable-to-trichotomous-least α (Pₒ , refl)) (decomposable-to-trichotomous-least β (𝟙ₒ , refl)) (inl ⋆ , (𝟙ₒ-↓ ⁻¹ ∙ +ₒ-↓-left ⋆)) f = [ β , α ×ₒ β ]⟨ 𝕗 ⟩ f-is-sim : is-simulation β (α ×ₒ β) f f-is-sim = [ β , α ×ₒ β ]⟨ 𝕗 ⟩-is-simulation I : (p : P) → f (inr ⋆) ＝ (inr p , inl ⋆) I p = ↓-lc (α ×ₒ β) (f (inr ⋆)) (inr p , inl ⋆) e where e = (α ×ₒ β) ↓ f (inr ⋆) ＝⟨ e₁ ⟩ β ↓ inr ⋆ ＝⟨ e₂ ⟩ 𝟙ₒ ＝⟨ e₃ ⟩ α ↓ inr p ＝⟨ e₄ ⟩ α ×ₒ 𝟘ₒ +ₒ (α ↓ inr p) ＝⟨ e₅ ⟩ α ×ₒ (β ↓ inl ⋆) +ₒ (α ↓ inr p) ＝⟨ ×ₒ-↓ α β ⁻¹ ⟩ (α ×ₒ β) ↓ (inr p , inl ⋆) ∎ where e₁ = (simulations-preserve-↓ β (α ×ₒ β) 𝕗 (inr ⋆)) ⁻¹ e₂ = +ₒ-↓-right ⋆ ⁻¹ ∙ ap (𝟙ₒ +ₒ_) 𝟙ₒ-↓ ∙ 𝟘ₒ-right-neutral 𝟙ₒ e₃ = (𝟘ₒ-right-neutral 𝟙ₒ) ⁻¹ ∙ ap (𝟙ₒ +ₒ_) ((prop-ordinal-↓ P-is-prop p) ⁻¹) ∙ +ₒ-↓-right p e₄ = (ap (_+ₒ (α ↓ inr p)) (×ₒ-𝟘ₒ-right α) ∙ 𝟘ₒ-left-neutral (α ↓ inr p)) ⁻¹ e₅ = ap (λ - → α ×ₒ - +ₒ (α ↓ inr p)) (𝟙ₒ-↓ ⁻¹ ∙ +ₒ-↓-left ⋆) II : (x : ⟨ α ⟩) → f (inr ⋆) ＝ (x , inr ⋆) → ¬ P II x e p = +disjoint (ap pr₂ ((I p) ⁻¹ ∙ e)) III : f (inr ⋆) ≠ (inl ⋆ , inl ⋆) III h = +disjoint (simulations-are-lc β (α ×ₒ β) f f-is-sim (e ∙ h ⁻¹)) where e : f (inl ⋆) ＝ (inl ⋆ , inl ⋆) e = simulations-preserve-least β (α ×ₒ β) (inl ⋆) (inl ⋆ , inl ⋆) f f-is-sim β-least (×ₒ-least α β (inl ⋆) (inl ⋆) (+ₒ-least 𝟙ₒ Pₒ ⋆ 𝟙ₒ-least) β-least) where β-least : is-least β (inl ⋆) β-least = +ₒ-least 𝟙ₒ 𝟙ₒ ⋆ 𝟙ₒ-least IV : (x : ⟨ α ×ₒ β ⟩) → f (inr ⋆) ＝ x → P + ¬ P IV (inl ⋆ , inl ⋆) e = 𝟘-elim (III e) IV (inr p , inl ⋆) e = inl p IV (inl ⋆ , inr ⋆) e = inr (II (inl ⋆) e) IV (inr p , inr ⋆) e = inl p ×ₒ-as-large-as-right-factor-implies-EM : ((α β : Ordinal 𝓤) → 𝟘ₒ ⊲ α → β ⊴ α ×ₒ β) → EM 𝓤 ×ₒ-as-large-as-right-factor-implies-EM hyp = ×ₒ-as-large-as-right-factor-implies-EM' (λ α β _ _ → hyp α β) EM-implies-×ₒ-as-large-as-right-factor : EM 𝓤 → (α β : Ordinal 𝓤) → 𝟘ₒ ⊲ α → β ⊴ α ×ₒ β EM-implies-×ₒ-as-large-as-right-factor em α β (a₀ , _) = ≼-gives-⊴ β (α ×ₒ β) (EM-implies-order-preserving-gives-≼ em β (α ×ₒ β) (f , I)) where f : ⟨ β ⟩ → ⟨ α ×ₒ β ⟩ f b = (a₀ , b) I : is-order-preserving β (α ×ₒ β) f I b b' l = inl lAdded in September 2025 by Fredrik Nordvall Forsberg. Moved here from ArithmeticReflection by Tom de Jong in October 2025. Some special cases of multiplication by ω.𝟙ₒ×ₒω-is-ω : 𝟙ₒ ×ₒ ω ＝ ω 𝟙ₒ×ₒω-is-ω = 𝟙ₒ-left-neutral-×ₒ ω 𝟚ₒ×ₒω-is-ω : 𝟚ₒ ×ₒ ω ＝ ω 𝟚ₒ×ₒω-is-ω = eqtoidₒ (ua _) fe' (𝟚ₒ ×ₒ ω) ω h where open import Naturals.Addition hiding (_+_) open import Naturals.Division open import Naturals.Order open import Naturals.Double f : ⟨ 𝟚ₒ ⟩ × ℕ → ℕ f (inl ⋆ , n) = double n f (inr ⋆ , n) = sdouble n g' : (n : ℕ) → division-theorem n 1 → ⟨ 𝟚ₒ ⟩ × ℕ g' n (k , 0 , p , l) = inl ⋆ , k g' n (k , 1 , p , l) = inr ⋆ , k g' n (k , succ (succ j) , p , l) = 𝟘-elim l g : ℕ → ⟨ 𝟚ₒ ⟩ × ℕ g n = g' n (division n 1) f-equiv : is-equiv f f-equiv = qinvs-are-equivs f (g , (η , ϵ)) where η' : (x : ⟨ 𝟚ₒ ⟩ × ℕ)(m : ℕ) → m ＝ f x → (d : division-theorem m 1) → g' m d ＝ x η' (inl ⋆ , n) m r (k , 0 , p , l) = ap (inl ⋆ ,_) (double-lc τ) where τ : double k ＝ double n τ = double-is-self-addition k ∙ p ⁻¹ ∙ r η' (inr ⋆ , n) m r (k , 0 , p , l) = 𝟘-elim (double-is-not-sdouble τ) where τ : double k ＝ sdouble n τ = double-is-self-addition k ∙ p ⁻¹ ∙ r η' (inl ⋆ , n) m r (k , 1 , p , l) = 𝟘-elim (double-is-not-sdouble τ) where τ : double n ＝ sdouble k τ = r ⁻¹ ∙ p ∙ ap succ (double-is-self-addition k ⁻¹) η' (inr ⋆ , n) m r (k , 1 , p , l) = ap (inr ⋆ ,_) (sdouble-lc τ) where τ : sdouble k ＝ sdouble n τ = ap succ (double-is-self-addition k) ∙ p ⁻¹ ∙ r η' (inl ⋆ , n) m r (k , succ (succ j) , p , l) = 𝟘-elim l η' (inr ⋆ , n) m r (k , succ (succ j) , p , l) = 𝟘-elim l η : (λ x → g (f x)) ∼ id η x = η' x (f x) refl (division (f x) 1) ϵ' : (n : ℕ) → (d : division-theorem n 1) → f (g' n d) ＝ n ϵ' n (k , 0 , refl , l) = double-is-self-addition k ϵ' n (k , 1 , refl , l) = ap succ (double-is-self-addition k) ϵ' n (k , succ (succ j) , p , l) = 𝟘-elim l ϵ : (λ n → f (g n)) ∼ id ϵ n = ϵ' n (division n 1) f-preserves-order : (x y : ⟨ 𝟚ₒ ⟩ × ℕ) → x ≺⟨ 𝟚ₒ ×ₒ ω ⟩ y → f x ≺⟨ ω ⟩ f y f-preserves-order (inl ⋆ , x) (inl ⋆ , y) (inl p) = transport₂⁻¹ (λ - → succ - ≤ℕ_) (double-is-self-addition x) (double-is-self-addition y) (≤-adding x y (succ x) y (≤-trans x (succ x) y (≤-succ x) p) p) f-preserves-order (inl ⋆ , x) (inr ⋆ , y) (inl p) = transport₂⁻¹ _≤ℕ_ (double-is-self-addition x) (double-is-self-addition y) (≤-adding x y x y (≤-trans x (succ x) y (≤-succ x) p) (≤-trans x (succ x) y (≤-succ x) p)) f-preserves-order (inr ⋆ , x) (inl ⋆ , y) (inl p) = transport₂⁻¹ (λ - → succ - ≤ℕ_) (ap succ (double-is-self-addition x) ∙ succ-left x x ⁻¹) (double-is-self-addition y) (≤-adding (succ x) y (succ x) y p p) f-preserves-order (inr ⋆ , x) (inr ⋆ , y) (inl p) = transport₂⁻¹ (λ - → succ - ≤ℕ_) (double-is-self-addition x) (double-is-self-addition y) (≤-adding x y (succ x) y (≤-trans x (succ x) y (≤-succ x) p) p) f-preserves-order (inl ⋆ , x) (inl ⋆ , y) (inr (refl , q)) = 𝟘-elim q f-preserves-order (inl ⋆ , x) (inr ⋆ , x) (inr (refl , _)) = ≤-refl _ f-preserves-order (inr ⋆ , x) (inl ⋆ , x) (inr (refl , q)) = 𝟘-elim q f-preserves-order (inr ⋆ , x) (inr ⋆ , x) (inr (refl , q)) = 𝟘-elim q f-reflects-order : (x y : ⟨ 𝟚ₒ ⟩ × ℕ) → f x ≺⟨ ω ⟩ f y → x ≺⟨ 𝟚ₒ ×ₒ ω ⟩ y f-reflects-order (inl ⋆ , x) (inl ⋆ , y) p = inl (double-reflects-< p) f-reflects-order (inl ⋆ , x) (inr ⋆ , y) p = τ (<-trichotomous x y) where τ : (x <ℕ y) + (x ＝ y) + (y <ℕ x) → (x <ℕ y) + (x ＝ y) × 𝟙 τ (inl l) = inl l τ (inr (inl e)) = inr (e , ⋆) τ (inr (inr g)) = 𝟘-elim (less-than-not-equal y y (<-≤-trans y x y g (double-reflects-≤ p)) refl) f-reflects-order (inr ⋆ , x) (inl ⋆ , y) p = inl (double-reflects-≤ p) f-reflects-order (inr ⋆ , x) (inr ⋆ , y) p = inl (double-reflects-< p) h : (𝟚ₒ ×ₒ ω) ≃ₒ ω h = f , order-preserving-reflecting-equivs-are-order-equivs (𝟚ₒ ×ₒ ω) ω f f-equiv f-preserves-order f-reflects-order