------------------------------------------------------------------------ -- The Agda standard library -- -- Additional properties for setoids ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (Setoid; Preorder; Poset) module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where open import Data.Product.Base using (_,_) open import Function.Base using (_∘_; id; _$_; flip) open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Construct.Composition using (_;_; impliesˡ; transitive⇒≈;≈⊆≈) open import Relation.Binary.Definitions using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Irreflexive) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open Setoid S ------------------------------------------------------------------------ -- Every setoid is a preorder and partial order with respect to -- propositional equality isPreorder : IsPreorder _≡_ _≈_ isPreorder = record { isEquivalence = record { refl = ≡.refl ; sym = ≡.sym ; trans = ≡.trans } ; reflexive = reflexive ; trans = trans } ≈-isPreorder : IsPreorder _≈_ _≈_ ≈-isPreorder = record { isEquivalence = isEquivalence ; reflexive = id ; trans = trans } ≈-isPartialOrder : IsPartialOrder _≈_ _≈_ ≈-isPartialOrder = record { isPreorder = ≈-isPreorder ; antisym = λ i≈j _ → i≈j } preorder : Preorder a a ℓ preorder = record { isPreorder = isPreorder } ≈-preorder : Preorder a ℓ ℓ ≈-preorder = record { isPreorder = ≈-isPreorder } ≈-poset : Poset a ℓ ℓ ≈-poset = record { isPartialOrder = ≈-isPartialOrder } ------------------------------------------------------------------------ -- Properties of _≉_ ≉-sym : Symmetric _≉_ ≉-sym x≉y = x≉y ∘ sym ≉-respˡ : _≉_ Respectsˡ _≈_ ≉-respˡ x≈x′ x≉y = x≉y ∘ trans x≈x′ ≉-respʳ : _≉_ Respectsʳ _≈_ ≉-respʳ y≈y′ x≉y x≈y′ = x≉y $ trans x≈y′ (sym y≈y′) ≉-resp₂ : _≉_ Respects₂ _≈_ ≉-resp₂ = ≉-respʳ , ≉-respˡ ≉-irrefl : Irreflexive _≈_ _≉_ ≉-irrefl x≈y x≉y = contradiction x≈y x≉y ------------------------------------------------------------------------ -- Equality is closed under composition ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ ≈;≈⇒≈ = transitive⇒≈;≈⊆≈ _ trans ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ ≈⇒≈;≈ = impliesˡ _≈_ _≈_ refl id ------------------------------------------------------------------------ -- Other properties respʳ-flip : _≈_ Respectsʳ (flip _≈_) respʳ-flip y≈z x≈z = trans x≈z (sym y≈z) respˡ-flip : _≈_ Respectsˡ (flip _≈_) respˡ-flip = trans