Martin Escardo, 20-21 December 2012. If X and Y come with orders, both denoted by ≤, then the lexicographic order on X × Y is defined by (x , y) ≤ (x' , y') ↔ x ≤ x' ∧ (x ＝ x' → y ≤ y'). More generally, we can consider the lexicographic product of two binary relations R on X and S on Y, which is a relation on X × Y, or even on (Σ x ꞉ X , Y x) if Y and S depend on X. \begin{code} {-# OPTIONS --safe --without-K #-} module Ordinals.LexicographicOrder where open import MLTT.Spartan open import UF.Base open import UF.Subsingletons lex-order : ∀ {𝓣} {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → (X → X → 𝓦 ̇ ) → ({x : X} → Y x → Y x → 𝓣 ̇ ) → (Σ Y → Σ Y → 𝓤 ⊔ 𝓦 ⊔ 𝓣 ̇ ) lex-order _≤_ _≼_ (x , y) (x' , y') = (x ≤ x') × ((r : x ＝ x') → transport _ r y ≼ y') \end{code} Added 14th June 2018, from 2013 in another development. However, for a strict order, it makes sense to define (x , y) < (x' , y') ↔ x < x' ∨ (x ＝ x' ∧ y < y'). \begin{code} slex-order : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } → (X → X → 𝓦 ̇ ) → ({x : X} → Y x → Y x → 𝓣 ̇ ) → (Σ Y → Σ Y → 𝓤 ⊔ 𝓦 ⊔ 𝓣 ̇ ) slex-order _<_ _≺_ (x , y) (x' , y') = (x < x') + (Σ r ꞉ x ＝ x' , transport _ r y ≺ y') \end{code} Usually in such a context, a ≤ b is defined to be ¬ (b < a). The negation of the strict lexicographic product is, then, ¬ (x < x') ∧ ¬ (x ＝ x' ∧ y < y') by de Morgan, ↔ x ≤ x' ∧ ¬ (x ＝ x' ∧ y < y') by definition of ≤, ↔ x' ≤ x ∧ ((x ＝ x' → ¬ (y < y')) by (un)currying, ↔ x' ≤ x ∧ ((x ＝ x' → y' ≤ y) by definition of ≤. What this means is that the non-strict lexigraphic product of the induced non-strict order is induced by the strict lexicographic product of the strict orders. This works a little more generally as follows. \begin{code} module lexicographic-commutation {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (_<_ : X → X → 𝓦 ̇ ) (_≺_ : {x : X} → Y x → Y x → 𝓣 ̇ ) (R : 𝓣 ̇ ) where not : ∀ {𝓤} → 𝓤 ̇ → 𝓣 ⊔ 𝓤 ̇ not A = A → R _⊏_ : Σ Y → Σ Y → 𝓣 ⊔ 𝓤 ⊔ 𝓦 ̇ _⊏_ = slex-order _<_ _≺_ _≤_ : X → X → 𝓦 ⊔ 𝓣 ̇ x ≤ x' = not (x' < x) _≼_ : {x : X} → Y x → Y x → 𝓣 ̇ y ≼ y' = not (y' ≺ y) _⊑_ : Σ Y → Σ Y → 𝓣 ⊔ 𝓤 ⊔ 𝓦 ̇ _⊑_ = lex-order _≤_ _≼_ forth : (x x' : X) (y : Y x) (y' : Y x') → not ((x , y) ⊏ (x' , y')) → (x' , y') ⊑ (x , y) forth x x' y y' f = g , h where g : not (x < x') g l = f (inl l) h : (r : x' ＝ x) → not (y ≺ transport Y r y') h refl l = f (inr (refl , l)) back : (x x' : X) (y : Y x) (y' : Y x') → (x' , y') ⊑ (x , y) → not ((x , y) ⊏ (x' , y')) back x x' y y' (g , h) (inl l) = g l back x _ y y' (g , h) (inr (refl , l)) = h refl l \end{code}