------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between orders
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Algebra.Morphism.Definitions
open import Function.Base
open import Data.Product.Base using (_,_; map)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Structures
  using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
open import Relation.Binary.Definitions
  using (Irreflexive; Antisymmetric; Trichotomous; tri<; tri≈; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
open import Relation.Binary.Morphism
import Relation.Binary.Morphism.RelMonomorphism as RawRelation

module Relation.Binary.Morphism.OrderMonomorphism
  {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Set a} {B : Set b}
  {_≈₁_ : Rel A ℓ₁} {_≈₂_ : Rel B ℓ₃}
  {_≲₁_ : Rel A ℓ₂} {_≲₂_ : Rel B ℓ₄}
  {⟦_⟧ : A → B}
  (isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧)
  where

open IsOrderMonomorphism isOrderMonomorphism

------------------------------------------------------------------------
-- Re-export equivalence proofs

module EqM = RawRelation Eq.isRelMonomorphism

open RawRelation isRelMonomorphism public

------------------------------------------------------------------------
-- Properties

reflexive : _≈₂_ ⇒ _≲₂_ → _≈₁_ ⇒ _≲₁_
reflexive refl x≈y = cancel (refl (cong x≈y))

irrefl : Irreflexive _≈₂_ _≲₂_ → Irreflexive _≈₁_ _≲₁_
irrefl irrefl x≈y x∼y = irrefl (cong x≈y) (mono x∼y)

antisym : Antisymmetric _≈₂_ _≲₂_ → Antisymmetric _≈₁_ _≲₁_
antisym antisym x∼y y∼x = injective (antisym (mono x∼y) (mono y∼x))

compare : Trichotomous _≈₂_ _≲₂_ → Trichotomous _≈₁_ _≲₁_
compare compare x y with compare ⟦ x ⟧ ⟦ y ⟧
... | tri< a ¬b ¬c = tri< (cancel a) (¬b ∘ cong) (¬c ∘ mono)
... | tri≈ ¬a b ¬c = tri≈ (¬a ∘ mono) (injective b) (¬c ∘ mono)
... | tri> ¬a ¬b c = tri> (¬a ∘ mono) (¬b ∘ cong) (cancel c)

respˡ : _≲₂_ Respectsˡ _≈₂_ → _≲₁_ Respectsˡ _≈₁_
respˡ resp x≈y x∼z = cancel (resp (cong x≈y) (mono x∼z))

respʳ : _≲₂_ Respectsʳ _≈₂_ → _≲₁_ Respectsʳ _≈₁_
respʳ resp x≈y y∼z = cancel (resp (cong x≈y) (mono y∼z))

resp : _≲₂_ Respects₂ _≈₂_ → _≲₁_ Respects₂ _≈₁_
resp = map respʳ respˡ

------------------------------------------------------------------------
-- Structures

isPreorder : IsPreorder _≈₂_ _≲₂_ → IsPreorder _≈₁_ _≲₁_
isPreorder O = record
  { isEquivalence = EqM.isEquivalence O.isEquivalence
  ; reflexive     = reflexive O.reflexive
  ; trans         = trans O.trans
  } where module O = IsPreorder O

isPartialOrder : IsPartialOrder _≈₂_ _≲₂_ → IsPartialOrder _≈₁_ _≲₁_
isPartialOrder O = record
  { isPreorder = isPreorder O.isPreorder
  ; antisym    = antisym O.antisym
  } where module O = IsPartialOrder O

isTotalOrder : IsTotalOrder _≈₂_ _≲₂_ → IsTotalOrder _≈₁_ _≲₁_
isTotalOrder O = record
  { isPartialOrder = isPartialOrder O.isPartialOrder
  ; total          = total O.total
  } where module O = IsTotalOrder O

isDecTotalOrder : IsDecTotalOrder _≈₂_ _≲₂_ → IsDecTotalOrder _≈₁_ _≲₁_
isDecTotalOrder O = record
  { isTotalOrder = isTotalOrder O.isTotalOrder
  ; _≟_          = EqM.dec O._≟_
  ; _≤?_         = dec O._≤?_
  } where module O = IsDecTotalOrder O

isStrictPartialOrder : IsStrictPartialOrder _≈₂_ _≲₂_ →
                       IsStrictPartialOrder _≈₁_ _≲₁_
isStrictPartialOrder O = record
  { isEquivalence = EqM.isEquivalence O.isEquivalence
  ; irrefl        = irrefl O.irrefl
  ; trans         = trans O.trans
  ; <-resp-≈      = resp O.<-resp-≈
  } where module O = IsStrictPartialOrder O

isStrictTotalOrder : IsStrictTotalOrder _≈₂_ _≲₂_ →
                     IsStrictTotalOrder _≈₁_ _≲₁_
isStrictTotalOrder O = record
  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
  ; compare              = compare O.compare
  } where module O = IsStrictTotalOrder O