```------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a strict partial order.

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Product.Relation.Binary.Lex.Strict where

open import Data.Product.Base
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
using (Pointwise)
open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
open import Data.Empty
open import Function.Base
open import Induction.WellFounded
open import Level
open import Relation.Nullary.Decidable
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)

private
variable
a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
A : Set a
B : Set b

------------------------------------------------------------------------
-- A lexicographic ordering over products

×-Lex : (_≈₁_ : Rel A ℓ₁) (_<₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
Rel (A × B) _
×-Lex _≈₁_ _<₁_ _≤₂_ =
(_<₁_ on proj₁) -⊎- (_≈₁_ on proj₁) -×- (_≤₂_ on proj₂)

------------------------------------------------------------------------
-- Some properties which are preserved by ×-Lex (under certain
-- assumptions).

×-reflexive : (_≈₁_ : Rel A ℓ₁) (_∼₁_ : Rel A ℓ₂)
{_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
_≈₂_ ⇒ _≤₂_ → (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
×-reflexive _ _ _ refl₂ = λ x≈y →
inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))

module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ₃} where

private
_<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_

×-transitive : IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ → Transitive _<₁_ →
Transitive _<₂_ → Transitive _<ₗₑₓ_
×-transitive eq₁ resp₁ trans₁ trans₂ = trans
where
module Eq₁ = IsEquivalence eq₁

trans : Transitive _<ₗₑₓ_
trans (inj₁ x₁<y₁) (inj₁ y₁<z₁) = inj₁ (trans₁ x₁<y₁ y₁<z₁)
trans (inj₁ x₁<y₁) (inj₂ y≈≤z)  =
inj₁ (proj₁ resp₁ (proj₁ y≈≤z) x₁<y₁)
trans (inj₂ x≈≤y)  (inj₁ y₁<z₁) =
inj₁ (proj₂ resp₁ (Eq₁.sym \$ proj₁ x≈≤y) y₁<z₁)
trans (inj₂ x≈≤y)  (inj₂ y≈≤z)  =
inj₂ ( Eq₁.trans (proj₁ x≈≤y) (proj₁ y≈≤z)
, trans₂    (proj₂ x≈≤y) (proj₂ y≈≤z))

×-asymmetric : Symmetric _≈₁_ → _<₁_ Respects₂ _≈₁_ →
Asymmetric _<₁_ → Asymmetric _<₂_ →
Asymmetric _<ₗₑₓ_
×-asymmetric sym₁ resp₁ asym₁ asym₂ = asym
where
irrefl₁ : Irreflexive _≈₁_ _<₁_
irrefl₁ = asym⇒irr resp₁ sym₁ asym₁

asym : Asymmetric _<ₗₑₓ_
asym (inj₁ x₁<y₁) (inj₁ y₁<x₁) = asym₁ x₁<y₁ y₁<x₁
asym (inj₁ x₁<y₁) (inj₂ y≈<x)  = irrefl₁ (sym₁ \$ proj₁ y≈<x) x₁<y₁
asym (inj₂ x≈<y)  (inj₁ y₁<x₁) = irrefl₁ (sym₁ \$ proj₁ x≈<y) y₁<x₁
asym (inj₂ x≈<y)  (inj₂ y≈<x)  = asym₂ (proj₂ x≈<y) (proj₂ y≈<x)

×-total₁ : Total _<₁_ → Total _<ₗₑₓ_
×-total₁ total₁ x y with total₁ (proj₁ x) (proj₁ y)
... | inj₁ x₁<y₁ = inj₁ (inj₁ x₁<y₁)
... | inj₂ x₁>y₁ = inj₂ (inj₁ x₁>y₁)

×-total₂ : Symmetric _≈₁_ →
Trichotomous _≈₁_ _<₁_ → Total _<₂_ →
Total _<ₗₑₓ_
×-total₂ sym tri₁ total₂ x y with tri₁ (proj₁ x) (proj₁ y)
... | tri< x₁<y₁ _ _ = inj₁ (inj₁ x₁<y₁)
... | tri> _ _ y₁<x₁ = inj₂ (inj₁ y₁<x₁)
... | tri≈ _ x₁≈y₁ _ with total₂ (proj₂ x) (proj₂ y)
...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁     , x₂≤y₂))
...   | inj₂ y₂≤x₂ = inj₂ (inj₂ (sym x₁≈y₁ , y₂≤x₂))

×-decidable : Decidable _≈₁_ → Decidable _<₁_ → Decidable _<₂_ →
Decidable _<ₗₑₓ_
×-decidable dec-≈₁ dec-<₁ dec-≤₂ x y =
dec-<₁ (proj₁ x) (proj₁ y)
⊎-dec
(dec-≈₁ (proj₁ x) (proj₁ y)
×-dec
dec-≤₂ (proj₂ x) (proj₂ y))

module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
{_≈₂_ : Rel B ℓ₃} {_<₂_ : Rel B ℓ₄} where

private
_≋_    = Pointwise _≈₁_ _≈₂_
_<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_

×-irreflexive : Irreflexive _≈₁_ _<₁_ → Irreflexive _≈₂_ _<₂_ →
Irreflexive (Pointwise _≈₁_ _≈₂_) _<ₗₑₓ_
×-irreflexive ir₁ ir₂ x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
×-irreflexive ir₁ ir₂ x≈y (inj₂ x≈<y)  = ir₂ (proj₂ x≈y) (proj₂ x≈<y)

×-antisymmetric : Symmetric _≈₁_ → Irreflexive _≈₁_ _<₁_ → Asymmetric _<₁_ →
Antisymmetric _≈₂_ _<₂_ → Antisymmetric _≋_ _<ₗₑₓ_
×-antisymmetric sym₁ irrefl₁ asym₁ antisym₂ = antisym
where
antisym : Antisymmetric _≋_ _<ₗₑₓ_
antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) =
⊥-elim \$ asym₁ x₁<y₁ y₁<x₁
antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  =
⊥-elim \$ irrefl₁ (sym₁ \$ proj₁ y≈≤x) x₁<y₁
antisym (inj₂ x≈≤y)  (inj₁ y₁<x₁) =
⊥-elim \$ irrefl₁ (sym₁ \$ proj₁ x≈≤y) y₁<x₁
antisym (inj₂ x≈≤y)  (inj₂ y≈≤x)  =
proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)

×-respectsʳ : Transitive _≈₁_ →
_<₁_ Respectsʳ _≈₁_ → _<₂_ Respectsʳ _≈₂_ →
_<ₗₑₓ_ Respectsʳ _≋_
×-respectsʳ trans resp₁ resp₂ y≈y' (inj₁ x₁<y₁) = inj₁ (resp₁ (proj₁ y≈y') x₁<y₁)
×-respectsʳ trans resp₁ resp₂ y≈y' (inj₂ x≈<y)  = inj₂ (trans (proj₁ x≈<y) (proj₁ y≈y')
, (resp₂ (proj₂ y≈y') (proj₂ x≈<y)))

×-respectsˡ : Symmetric _≈₁_ → Transitive _≈₁_ →
_<₁_ Respectsˡ _≈₁_ → _<₂_ Respectsˡ _≈₂_ →
_<ₗₑₓ_ Respectsˡ _≋_
×-respectsˡ sym trans resp₁ resp₂ x≈x' (inj₁ x₁<y₁) = inj₁ (resp₁ (proj₁ x≈x') x₁<y₁)
×-respectsˡ sym trans resp₁ resp₂ x≈x' (inj₂ x≈<y)  = inj₂ (trans (sym \$ proj₁ x≈x') (proj₁ x≈<y)
, (resp₂ (proj₂ x≈x') (proj₂ x≈<y)))

×-respects₂ : IsEquivalence _≈₁_ →
_<₁_ Respects₂ _≈₁_ → _<₂_ Respects₂ _≈₂_ →
_<ₗₑₓ_ Respects₂ _≋_
×-respects₂ eq₁ resp₁ resp₂ = ×-respectsʳ trans (proj₁ resp₁) (proj₁ resp₂)
, ×-respectsˡ sym trans (proj₂ resp₁) (proj₂ resp₂)
where open IsEquivalence eq₁

×-compare : Symmetric _≈₁_ →
Trichotomous _≈₁_ _<₁_ → Trichotomous _≈₂_ _<₂_ →
Trichotomous _≋_ _<ₗₑₓ_
×-compare sym₁ cmp₁ cmp₂ (x₁ , x₂) (y₁ , y₂) with cmp₁ x₁ y₁
... | (tri< x₁<y₁ x₁≉y₁ x₁≯y₁) =
tri< (inj₁ x₁<y₁)
(x₁≉y₁ ∘ proj₁)
[ x₁≯y₁ , x₁≉y₁ ∘ sym₁ ∘ proj₁ ]
... | (tri> x₁≮y₁ x₁≉y₁ x₁>y₁) =
tri> [ x₁≮y₁ , x₁≉y₁ ∘ proj₁ ]
(x₁≉y₁ ∘ proj₁)
(inj₁ x₁>y₁)
... | (tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁) with cmp₂ x₂ y₂
...   | (tri< x₂<y₂ x₂≉y₂ x₂≯y₂) =
tri< (inj₂ (x₁≈y₁ , x₂<y₂))
(x₂≉y₂ ∘ proj₂)
[ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
...   | (tri> x₂≮y₂ x₂≉y₂ x₂>y₂) =
tri> [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
(x₂≉y₂ ∘ proj₂)
(inj₂ (sym₁ x₁≈y₁ , x₂>y₂))
...   | (tri≈ x₂≮y₂ x₂≈y₂ x₂≯y₂) =
tri≈ [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
(x₁≈y₁ , x₂≈y₂)
[ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]

module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ₃} where

private
_<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_

×-wellFounded' : Symmetric _≈₁_ → Transitive _≈₁_ →
_<₁_ Respectsʳ _≈₁_ →
WellFounded _<₁_ →
WellFounded _<₂_ →
WellFounded _<ₗₑₓ_
×-wellFounded' sym trans resp wf₁ wf₂ (x , y) = acc (×-acc (wf₁ x) (wf₂ y))
where
×-acc : ∀ {x y} →
Acc _<₁_ x → Acc _<₂_ y →
WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y)
×-acc (acc rec₁) acc₂ (u , v) (inj₁ u<x)
= acc (×-acc (rec₁ u u<x) (wf₂ v))
×-acc {x₁} acc₁ (acc rec₂) (u , v) (inj₂ (u≈x , v<y))
= Acc-resp-≈ (Pointwise.×-symmetric {_∼₁_ = _≈₁_} {_∼₂_ = _≡_ } sym ≡.sym)
(×-respectsʳ {_<₁_ = _<₁_} {_<₂_ = _<₂_} trans resp (≡.respʳ _<₂_))
(sym u≈x , _≡_.refl)
(acc (×-acc acc₁ (rec₂ v v<y)))

module _ {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel B ℓ₂} where

private
_<ₗₑₓ_ = ×-Lex _≡_ _<₁_ _<₂_

×-wellFounded : WellFounded _<₁_ →
WellFounded _<₂_ →
WellFounded _<ₗₑₓ_
×-wellFounded = ×-wellFounded' ≡.sym ≡.trans (≡.respʳ _<₁_)

------------------------------------------------------------------------
-- Collections of properties which are preserved by ×-Lex.

module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
{_≈₂_ : Rel B ℓ₃} {_<₂_ : Rel B ℓ₄} where

private
_≋_    = Pointwise _≈₁_ _≈₂_
_<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_

×-isPreorder : IsPreorder _≈₁_ _<₁_ →
IsPreorder _≈₂_ _<₂_ →
IsPreorder _≋_ _<ₗₑₓ_
×-isPreorder pre₁ pre₂ =
record
{ isEquivalence = Pointwise.×-isEquivalence
(isEquivalence pre₁) (isEquivalence pre₂)
; reflexive     = ×-reflexive _≈₁_ _<₁_ _<₂_ (reflexive pre₂)
; trans         = ×-transitive {_<₂_ = _<₂_}
(isEquivalence pre₁) (∼-resp-≈ pre₁)
(trans pre₁) (trans pre₂)
}
where open IsPreorder

×-isStrictPartialOrder : IsStrictPartialOrder _≈₁_ _<₁_ →
IsStrictPartialOrder _≈₂_ _<₂_ →
IsStrictPartialOrder _≋_ _<ₗₑₓ_
×-isStrictPartialOrder spo₁ spo₂ =
record
{ isEquivalence = Pointwise.×-isEquivalence
(isEquivalence spo₁) (isEquivalence spo₂)
; irrefl        = ×-irreflexive {_<₁_ = _<₁_} {_<₂_ = _<₂_}
(irrefl spo₁) (irrefl spo₂)
; trans         = ×-transitive {_<₁_ = _<₁_} {_<₂_ = _<₂_}
(isEquivalence spo₁)
(<-resp-≈ spo₁) (trans spo₁)
(trans spo₂)
; <-resp-≈      = ×-respects₂ (isEquivalence spo₁)
(<-resp-≈ spo₁)
(<-resp-≈ spo₂)
}
where open IsStrictPartialOrder

×-isStrictTotalOrder : IsStrictTotalOrder _≈₁_ _<₁_ →
IsStrictTotalOrder _≈₂_ _<₂_ →
IsStrictTotalOrder _≋_ _<ₗₑₓ_
×-isStrictTotalOrder spo₁ spo₂ =
record
{ isEquivalence = Pointwise.×-isEquivalence
(isEquivalence spo₁) (isEquivalence spo₂)
; trans         = ×-transitive {_<₁_ = _<₁_} {_<₂_ = _<₂_}
(isEquivalence spo₁)
(<-resp-≈ spo₁) (trans spo₁)
(trans spo₂)
; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
(compare spo₂)
}
where open IsStrictTotalOrder

------------------------------------------------------------------------
-- "Bundles" can also be combined.

×-preorder : Preorder a ℓ₁ ℓ₂ →
Preorder b ℓ₃ ℓ₄ →
Preorder _ _ _
×-preorder p₁ p₂ = record
{ isPreorder = ×-isPreorder (isPreorder p₁) (isPreorder p₂)
} where open Preorder

×-strictPartialOrder : StrictPartialOrder a ℓ₁ ℓ₂ →
StrictPartialOrder b ℓ₃ ℓ₄ →
StrictPartialOrder _ _ _
×-strictPartialOrder s₁ s₂ = record
{ isStrictPartialOrder = ×-isStrictPartialOrder
(isStrictPartialOrder s₁) (isStrictPartialOrder s₂)
} where open StrictPartialOrder

×-strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ →
StrictTotalOrder b ℓ₃ ℓ₄ →
StrictTotalOrder _ _ _
×-strictTotalOrder s₁ s₂ = record
{ isStrictTotalOrder = ×-isStrictTotalOrder
(isStrictTotalOrder s₁) (isStrictTotalOrder s₂)
} where open StrictTotalOrder
```