------------------------------------------------------------------------
-- 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 Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Morphism using (IsOrderMonomorphism)
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 import Function.Base using (flip; _∘_)
open import Data.Product.Base using (_,_; map)
open import Relation.Binary.Definitions
using (Irreflexive; Antisymmetric; Trichotomous; tri<; tri≈; tri>
; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
import Relation.Binary.Morphism.RelMonomorphism as RawRelation
using (isEquivalence; trans; total; dec)
open import Relation.Binary.Structures
using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder
; IsStrictPartialOrder; IsStrictTotalOrder)
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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4