------------------------------------------------------------------------
-- Induced preorders
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

open import Relation.Binary

module Relation.Binary.InducedPreorders
         {s₁ s₂}
         (S : Setoid s₁ s₂)  -- The underlying equality.
         where

open import Function
open import Data.Product

open Setoid S

-- Every respectful unary relation induces a preorder. (No claim is
-- made that this preorder is unique.)

InducedPreorder₁ : ∀ {p} (P : Carrier → Set p) →
                   P Respects _≈_ → Preorder _ _ _
InducedPreorder₁ P resp = record
  { _≈_        = _≈_
  ; _∼_        = λ c₁ c₂ → P c₁ → P c₂
  ; isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = resp
    ; trans         = flip _∘′_
    ; ∼-resp-≈      = (λ c₁≈c₂ c₃∼c₁ → resp c₁≈c₂ ∘ c₃∼c₁)
                    , (λ c₁≈c₂ c₁∼c₃ → c₁∼c₃ ∘ resp (sym c₁≈c₂))
    }
  }

-- Every respectful binary relation induces a preorder. (No claim is
-- made that this preorder is unique.)

InducedPreorder₂ : ∀ {a r} {A : Set a} →
                   (_R_ : A → Carrier → Set r) →
                   (∀ {x} → _R_ x Respects _≈_) → Preorder _ _ _
InducedPreorder₂ _R_ resp = record
  { _≈_        = _≈_
  ; _∼_        = λ c₁ c₂ → ∀ {a} → a R c₁ → a R c₂
  ; isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = λ c₁≈c₂ → resp c₁≈c₂
    ; trans         = λ c₁∼c₂ c₂∼c₃ → c₂∼c₃ ∘ c₁∼c₂
    ; ∼-resp-≈      = (λ c₁≈c₂ c₃∼c₁ → resp c₁≈c₂ ∘ c₃∼c₁)
                    , (λ c₁≈c₂ c₁∼c₃ → c₁∼c₃ ∘ resp (sym c₁≈c₂))
    }
  }