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

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

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

module Relation.Binary.Construct.FromRel
  {s₁ s₂} (S : Setoid s₁ s₂)                    -- The underlying equality
  {a r} {A : Set a} (_R_ : REL A (Carrier S) r) -- The relation
  where

open import Function.Base
open import Level using (_⊔_)

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

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

Resp : Rel B (a ⊔ r)
Resp x y = ∀ {a} → a R x → a R y

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

reflexive : (∀ {a} → (a R_) Respects _≈_) → _≈_ ⇒ Resp
reflexive resp x≈y = resp x≈y

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

isPreorder : (∀ {a} → (a R_) Respects _≈_) → IsPreorder _≈_ Resp
isPreorder resp = record
  { isEquivalence = Eq.isEquivalence
  ; reflexive     = reflexive resp
  ; trans         = trans
  }

preorder : (∀ {a} → (a R_) Respects _≈_) → Preorder _ _ _
preorder resp = record
  { isPreorder = isPreorder resp
  }