    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Every respectful unary relation induces a preorder. No claim is
    -- made that this preorder is unique.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Core using (Rel; _⇒_)
    open import Relation.Binary.Bundles using (Setoid; Preorder)
    open import Relation.Binary.Structures using (IsPreorder)
    open import Relation.Binary.Definitions using (_Respects_; Reflexive; Transitive)
    open import Relation.Unary using (Pred)

    module Relation.Binary.Construct.FromPred
      {s₁ s₂} (S : Setoid s₁ s₂)          -- The underlying equality
      {p} (P : Pred (Setoid.Carrier S) p) -- The predicate
      where

    open import Function.Base

    open module Eq = Setoid S using (_≈_) renaming (Carrier to A)

    ------------------------------------------------------------------------
    -- Definition

    Resp : Rel A p
    Resp x y = P x → P y

    ------------------------------------------------------------------------
    -- Properties

    reflexive : P Respects _≈_ → _≈_ ⇒ Resp
    reflexive resp = resp

    refl : P Respects _≈_ → Reflexive Resp
    refl resp = resp Eq.refl

    trans : Transitive Resp
    trans x⇒y y⇒z = y⇒z ∘ x⇒y

    isPreorder : P Respects _≈_ → IsPreorder _≈_ Resp
    isPreorder resp = record
      { isEquivalence = Eq.isEquivalence
      ; reflexive     = reflexive resp
      ; trans         = flip _∘′_
      }

    preorder : P Respects _≈_ → Preorder _ _ _
    preorder resp = record
      { isPreorder = isPreorder resp
      }