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}