------------------------------------------------------------------------
-- 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 using (_,_; map)
open import Relation.Binary
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
  { isEquivalence = EqM.isEquivalence O.isEquivalence
  ; trans         = trans O.trans
  ; compare       = compare O.compare
  } where module O = IsStrictTotalOrder O