module Data.Product.Relation.Lex.NonStrict 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 Data.Product.Relation.Pointwise.NonDependent as Pointwise
using (Pointwise)
import Data.Product.Relation.Lex.Strict as Strict
module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
×-Lex : (_≈₁_ _≤₁_ : Rel A₁ ℓ₁) (_≤₂_ : Rel A₂ ℓ₂) → Rel (A₁ × A₂) _
×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_
×-reflexive : ∀ _≈₁_ _≤₁_ {_≈₂_} _≤₂_ →
_≈₂_ ⇒ _≤₂_ →
(Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂
×-transitive : ∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
∀ {_≤₂_} → Transitive _≤₂_ →
Transitive (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-transitive {_≈₁_} {_≤₁_} po₁ {_≤₂_} trans₂ =
Strict.×-transitive
{_<₁_ = Conv._<_ _≈₁_ _≤₁_}
isEquivalence (Conv.<-resp-≈ _ _ isEquivalence ≤-resp-≈)
(Conv.trans _ _ po₁)
{_≤₂_} trans₂
where open IsPartialOrder po₁
×-antisymmetric :
∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → Antisymmetric _≈₂_ _≤₂_ →
Antisymmetric (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-antisymmetric {_≈₁_} {_≤₁_}
po₁ {_≤₂_ = _≤₂_} antisym₂ =
Strict.×-antisymmetric {_<₁_ = Conv._<_ _≈₁_ _≤₁_}
≈-sym₁ irrefl₁ asym₁
{_≤₂_ = _≤₂_} antisym₂
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₂ (Pointwise _≈₁_ _≈₂_)
×-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₂))
×-isPartialOrder :
∀ {_≈₁_ _≤₁_} → IsPartialOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → IsPartialOrder _≈₂_ _≤₂_ →
IsPartialOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-isPartialOrder {_≈₁_} {_≤₁_} po₁
{_≤₂_ = _≤₂_} po₂ = record
{ isPreorder = record
{ isEquivalence = Pointwise.×-isEquivalence
(isEquivalence po₁)
(isEquivalence po₂)
; reflexive = ×-reflexive _≈₁_ _≤₁_ _≤₂_ (reflexive po₂)
; trans = ×-transitive po₁ {_≤₂_ = _≤₂_} (trans po₂)
}
; antisym = ×-antisymmetric {_≤₁_ = _≤₁_} po₁
{_≤₂_ = _≤₂_} (antisym po₂)
}
where open IsPartialOrder
×-isTotalOrder :
∀ {_≈₁_ _≤₁_} → Decidable _≈₁_ → IsTotalOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → IsTotalOrder _≈₂_ _≤₂_ →
IsTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-isTotalOrder {_≤₁_ = _≤₁_} ≈₁-dec to₁ {_≤₂_ = _≤₂_} to₂ = record
{ isPartialOrder = ×-isPartialOrder
(isPartialOrder to₁) (isPartialOrder to₂)
; total = ×-total {_≤₁_ = _≤₁_} (Eq.sym to₁) ≈₁-dec
(antisym to₁) (total to₁)
{_≤₂_ = _≤₂_} (total to₂)
}
where open IsTotalOrder
×-isDecTotalOrder :
∀ {_≈₁_ _≤₁_} → IsDecTotalOrder _≈₁_ _≤₁_ →
∀ {_≈₂_ _≤₂_} → IsDecTotalOrder _≈₂_ _≤₂_ →
IsDecTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _≤₁_ _≤₂_)
×-isDecTotalOrder {_≤₁_ = _≤₁_} to₁ {_≤₂_ = _≤₂_} to₂ = record
{ isTotalOrder = ×-isTotalOrder (_≟_ to₁)
(isTotalOrder to₁)
(isTotalOrder to₂)
; _≟_ = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
; _≤?_ = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
}
where open IsDecTotalOrder
module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where
×-poset : Poset ℓ₁ ℓ₂ _ → Poset ℓ₃ ℓ₄ _ → Poset _ _ _
×-poset p₁ p₂ = record
{ isPartialOrder = ×-isPartialOrder
(isPartialOrder p₁) (isPartialOrder p₂)
} where open Poset
×-totalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → TotalOrder ℓ₃ ℓ₄ _ →
TotalOrder _ _ _
×-totalOrder t₁ t₂ = record
{ isTotalOrder = ×-isTotalOrder T₁._≟_ T₁.isTotalOrder T₂.isTotalOrder
}
where
module T₁ = DecTotalOrder t₁
module T₂ = TotalOrder t₂
×-decTotalOrder : DecTotalOrder ℓ₁ ℓ₂ _ → DecTotalOrder ℓ₃ ℓ₄ _ →
DecTotalOrder _ _ _
×-decTotalOrder t₁ t₂ = record
{ isDecTotalOrder = ×-isDecTotalOrder
(isDecTotalOrder t₁) (isDecTotalOrder t₂)
} where open DecTotalOrder
_×-isPartialOrder_ = ×-isPartialOrder
_×-isDecTotalOrder_ = ×-isDecTotalOrder
_×-poset_ = ×-poset
_×-totalOrder_ = ×-totalOrder
_×-decTotalOrder_ = ×-decTotalOrder
×-≈-respects₂ = ×-respects₂