------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between binary relations
------------------------------------------------------------------------
-- 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 (IsRelMonomorphism)
module Relation.Binary.Morphism.RelMonomorphism
{a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
{_∼₁_ : Rel A ℓ₁} {_∼₂_ : Rel B ℓ₂}
{⟦_⟧ : A → B} (isMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧)
where
open import Data.Sum.Base as Sum using (map)
open import Function.Base using (flip; _∘_)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive; Total; Asymmetric; Decidable)
open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence)
open import Relation.Nullary.Decidable.Core using (yes; no; map′)
open IsRelMonomorphism isMonomorphism
------------------------------------------------------------------------
-- Properties
refl : Reflexive _∼₂_ → Reflexive _∼₁_
refl refl = injective refl
sym : Symmetric _∼₂_ → Symmetric _∼₁_
sym sym x∼y = injective (sym (cong x∼y))
trans : Transitive _∼₂_ → Transitive _∼₁_
trans trans x∼y y∼z = injective (trans (cong x∼y) (cong y∼z))
total : Total _∼₂_ → Total _∼₁_
total total x y = Sum.map injective injective (total ⟦ x ⟧ ⟦ y ⟧)
asym : Asymmetric _∼₂_ → Asymmetric _∼₁_
asym asym x∼y y∼x = asym (cong x∼y) (cong y∼x)
dec : Decidable _∼₂_ → Decidable _∼₁_
dec _∼?_ x y = map′ injective cong (⟦ x ⟧ ∼? ⟦ y ⟧)
------------------------------------------------------------------------
-- Structures
isEquivalence : IsEquivalence _∼₂_ → IsEquivalence _∼₁_
isEquivalence isEq = record
{ refl = refl E.refl
; sym = sym E.sym
; trans = trans E.trans
} where module E = IsEquivalence isEq
isDecEquivalence : IsDecEquivalence _∼₂_ → IsDecEquivalence _∼₁_
isDecEquivalence isDecEq = record
{ isEquivalence = isEquivalence E.isEquivalence
; _≟_ = dec E._≟_
} where module E = IsDecEquivalence isDecEq
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