```------------------------------------------------------------------------
-- The Agda standard library
--
-- Additional properties for setoids
------------------------------------------------------------------------

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

open import Data.Product.Base using (_,_)
open import Function.Base using (_∘_; id; _\$_; flip)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
open import Relation.Binary.Definitions
using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder)

module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where

open Setoid S

------------------------------------------------------------------------
-- Every setoid is a preorder and partial order with respect to
-- propositional equality

isPreorder : IsPreorder _≡_ _≈_
isPreorder = record
{ isEquivalence = record
{ refl  = P.refl
; sym   = P.sym
; trans = P.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ˡ

------------------------------------------------------------------------
-- 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
```