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.

\begin{code}

{-# 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)

\end{code}

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.

\begin{code}

×ₒ-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)))

\end{code}

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.

\begin{code}

×ₒ-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)

\end{code}

The following characterizes the initial segments of a product and is rather
useful when working with simulations between products.

\begin{code}

×ₒ-↓ : (α β : 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)

\end{code}

We now prove several useful facts about (bounded) simulations between products.

\begin{code}

×ₒ-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)

\end{code}

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).

\begin{code}

×ₒ-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)

\end{code}

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.

\begin{code}

×ₒ-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 α γ δ 𝕗)

\end{code}

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 ＝.

\begin{code}

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₀) ∎)
             𝕗)

\end{code}

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

\begin{code}

×ₒ-left-cancellable : (α β γ : Ordinal 𝓤)
                    → 𝟘ₒ ⊲ α
                    → (α ×ₒ β) ＝ (α ×ₒ γ)
                    → β ＝ γ
×ₒ-left-cancellable {𝓤 = 𝓤} α β γ p e = ⊴-antisym β γ (f β γ e) (f γ β (e ⁻¹))
 where
  f : (β γ : Ordinal 𝓤) → (α ×ₒ β) ＝ (α ×ₒ γ) → β ⊴ γ
  f β γ e = ×ₒ-left-cancellable-⊴ α β γ p (≃ₒ-to-⊴ (α ×ₒ β) (α ×ₒ γ)
                                                   (idtoeqₒ (α ×ₒ β) (α ×ₒ γ) e))

\end{code}

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).

\begin{code}

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')               ∎
\end{code}

Using similar techniques, we can also prove that multiplication is
left cancellable with respect to ⊲.

\begin{code}

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 II

\end{code}

Added 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.

\begin{code}

×ₒ-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 l

\end{code}

Added in September 2025 by Fredrik Nordvall Forsberg.
Moved here from ArithmeticReflection by Tom de Jong in October 2025.

Some special cases of multiplication by ω.

\begin{code}

𝟙ₒ×ₒω-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  → ⟨ 𝟚ₒ ⟩ × ℕ
  g' n (k ,  , p , l) = inl ⋆ , k
  g' n (k ,  , p , l) = inr ⋆ , k
  g' n (k , succ (succ j) , p , l) = 𝟘-elim l

  g : ℕ → ⟨ 𝟚ₒ ⟩ × ℕ
  g n = g' n (division n )

  f-equiv : is-equiv f
  f-equiv = qinvs-are-equivs f (g , (η , ϵ))
   where
    η' : (x : ⟨ 𝟚ₒ ⟩ × ℕ)(m : ℕ) → m ＝ f x → (d : division-theorem m )
       → g' m d ＝ x
    η' (inl ⋆ , n) m r (k ,  , p , l) = ap (inl ⋆ ,_) (double-lc τ)
     where
      τ : double k ＝ double n
      τ = double-is-self-addition k ∙ p ⁻¹ ∙ r
    η' (inr ⋆ , n) m r (k ,  , p , l) = 𝟘-elim (double-is-not-sdouble τ)
     where
      τ : double k ＝ sdouble n
      τ = double-is-self-addition k ∙ p ⁻¹  ∙ r
    η' (inl ⋆ , n) m r (k ,  , 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 ,  , 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) )

    ϵ' : (n : ℕ) → (d : division-theorem n ) → f (g' n d) ＝ n
    ϵ' n (k ,  , refl , l) = double-is-self-addition k
    ϵ' n (k ,  , 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 )

  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

\end{code}