```------------------------------------------------------------------------
-- 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 (non-strict) partial order.

module Relation.Binary.Product.NonStrictLex where

open import Data.Product
open import Data.Sum
open import Level
open import Relation.Binary
open import Relation.Binary.Consequences
import Relation.Binary.NonStrictToStrict as Conv
open import Relation.Binary.Product.Pointwise as Pointwise
using (_×-Rel_)
import Relation.Binary.Product.StrictLex as Strict

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁) → (_≤₂_ : Rel A₂ ℓ₂) →
Rel (A₁ × A₂) _
×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_

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

×-reflexive : ∀ _≈₁_ _≤₁_ {_≈₂_} _≤₂_ →
_≈₂_ ⇒ _≤₂_ → (_≈₁_ ×-Rel _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ {x} {y} =
Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂ {x} {y}

×-transitive : ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
∀ {_≤₂_} → Transitive _≤₂_ →
Transitive (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-transitive {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} po₁ {_≤₂_ = _≤₂_} trans₂
{x} {y} {z} =
Strict.×-transitive
{_<₁_ = Conv._<_ _≈₁_ _≤₁_}
isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
(Conv.trans _ _ po₁)
{_≤₂_ = _≤₂_} trans₂ {x} {y} {z}
where open IsPartialOrder po₁

×-antisymmetric :
∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → Antisymmetric _≈₂_ _≤₂_ →
Antisymmetric (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-antisymmetric {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_}
po₁ {_≤₂_ = _≤₂_} antisym₂ {x} {y} =
Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
≈-sym₁ irrefl₁ asym₁
{_≤₂_ = _≤₂_} antisym₂ {x} {y}
where
open IsPartialOrder po₁
open Eq renaming (refl to ≈-refl₁; sym to ≈-sym₁)

irrefl₁ : Irreflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
irrefl₁ = Conv.irrefl _≈₁_ _≤₁_

asym₁ : Asymmetric (Conv._<_ _≈₁_ _≤₁_)
asym₁ = trans∧irr⟶asym {_≈_ = _≈₁_}
≈-refl₁ (Conv.trans _ _ po₁) irrefl₁

×-≈-respects₂ :
∀ {_≈₁_ _≤₁_} → IsEquivalence _≈₁_ → _≤₁_ Respects₂ _≈₁_ →
∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} → _≤₂_ Respects₂ _≈₂_ →
(×-Lex _≈₁_ _≤₁_ _≤₂_) Respects₂ (_≈₁_ ×-Rel _≈₂_)
×-≈-respects₂ eq₁ resp₁ resp₂ =
Strict.×-≈-respects₂ eq₁ (Conv.<-resp-≈ _ _ eq₁ resp₁) resp₂

×-decidable : ∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → Decidable _≤₁_ →
∀ {_≤₂_} → Decidable _≤₂_ →
Decidable (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
Strict.×-decidable dec-≈₁ (Conv.decidable _ _ dec-≈₁ dec-≤₁)
dec-≤₂

×-total : ∀ {_≈₁_ _≤₁_} → Symmetric _≈₁_ → Decidable _≈₁_ →
Antisymmetric _≈₁_ _≤₁_ → Total _≤₁_ →
∀ {_≤₂_} → Total _≤₂_ →
Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-total {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} sym₁ dec₁ antisym₁ total₁
{_≤₂_ = _≤₂_} total₂ = total
where
tri₁ : Trichotomous _≈₁_ (Conv._<_ _≈₁_ _≤₁_)
tri₁ = Conv.trichotomous _ _ sym₁ dec₁ antisym₁ total₁

total : Total (×-Lex _≈₁_ _≤₁_ _≤₂_)
total x y with tri₁ (proj₁ x) (proj₁ y)
... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = inj₁ (inj₁ x₁<y₁)
... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = inj₂ (inj₁ x₁>y₁)
... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with total₂ (proj₂ x) (proj₂ y)
...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))

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

_×-isPartialOrder_ :
∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → IsPartialOrder _≈₂_ _≤₂_ →
IsPartialOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
_×-isPartialOrder_ {_≈₁_ = _≈₁_} {_≤₁_ = _≤₁_} po₁
{_≤₂_ = _≤₂_} po₂ = record
{ isPreorder = record
{ isEquivalence = Pointwise._×-isEquivalence_
(isEquivalence po₁)
(isEquivalence po₂)
; reflexive     = λ {x y} →
×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
{x} {y}
; trans         = λ {x y z} →
×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
{x} {y} {z}
}
; antisym = λ {x y} →
×-antisymmetric {_≤₁_ = _≤₁_} po₁
{_≤₂_ = _≤₂_} (antisym po₂) {x} {y}
}
where open IsPartialOrder

×-isTotalOrder :
∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → IsTotalOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → IsTotalOrder _≈₂_ _≤₂_ →
IsTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-isTotalOrder {_≤₁_ = _≤₁_} ≈₁-dec to₁ {_≤₂_ = _≤₂_} to₂ = record
{ isPartialOrder = isPartialOrder to₁ ×-isPartialOrder
isPartialOrder to₂
; total          = ×-total {_≤₁_ = _≤₁_} (Eq.sym to₁) ≈₁-dec
(antisym to₁) (total to₁)
{_≤₂_ = _≤₂_} (total to₂)
}
where open IsTotalOrder

_×-isDecTotalOrder_ :
∀ {_≈₁_ _≤₁_} → IsDecTotalOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → IsDecTotalOrder _≈₂_ _≤₂_ →
IsDecTotalOrder (_≈₁_ ×-Rel _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
_×-isDecTotalOrder_ {_≤₁_ = _≤₁_} to₁ {_≤₂_ = _≤₂_} to₂ = record
{ isTotalOrder = ×-isTotalOrder (_≟_ to₁)
(isTotalOrder to₁)
(isTotalOrder to₂)
; _≟_          = Pointwise._×-decidable_ (_≟_ to₁) (_≟_ to₂)
; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
}
where open IsDecTotalOrder

-- "Packages" (e.g. posets) can also be combined.

_×-poset_ :
∀ {p₁ p₂ p₃ p₄} → Poset p₁ p₂ _ → Poset p₃ p₄ _ → Poset _ _ _
p₁ ×-poset p₂ = record
{ isPartialOrder = isPartialOrder p₁ ×-isPartialOrder
isPartialOrder p₂
} where open Poset

_×-totalOrder_ :
∀ {d₁ d₂ t₃ t₄} →
DecTotalOrder d₁ d₂ _ → TotalOrder t₃ t₄ _ → TotalOrder _ _ _
t₁ ×-totalOrder t₂ = record
{ isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
}
where
module T₁ = DecTotalOrder t₁
module T₂ =    TotalOrder t₂

_×-decTotalOrder_ :
∀ {d₁ d₂ d₃ d₄} →
DecTotalOrder d₁ d₂ _ → DecTotalOrder d₃ d₄ _ → DecTotalOrder _ _ _
t₁ ×-decTotalOrder t₂ = record
{ isDecTotalOrder = isDecTotalOrder t₁ ×-isDecTotalOrder
isDecTotalOrder t₂
} where open DecTotalOrder
```