------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by preorders
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Bundles using (Preorder; Setoid)
open import Relation.Binary.Structures using (IsPreorder)
 
module Relation.Binary.Properties.Preorder
  {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where
 
open import Function.Base using (flip)
open import Data.Product.Base as Product using (_×_; _,_; swap)
import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 
open Preorder P
 
 
------------------------------------------------------------------------
-- The converse relation is also a preorder.
 
converse-isPreorder : IsPreorder _≈_ _≳_
converse-isPreorder = EqAndOrd.isPreorder isPreorder
 
converse-preorder : Preorder p₁ p₂ p₃
converse-preorder = EqAndOrd.preorder P
 
------------------------------------------------------------------------
-- For every preorder there is an induced equivalence
 
InducedEquivalence : Setoid _ _
InducedEquivalence = record
  { _≈_           = λ x y → x ≲ y × x ≳ y
  ; isEquivalence = record
    { refl  = (refl , refl)
    ; sym   = swap
    ; trans = Product.zip trans (flip trans)
    }
  }
 
 
 
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
 
-- Version 2.0
 
invIsPreorder = converse-isPreorder
{-# WARNING_ON_USAGE invIsPreorder
"Warning: invIsPreorder was deprecated in v2.0.
Please use converse-isPreorder instead."
#-}
invPreorder = converse-preorder
{-# WARNING_ON_USAGE invPreorder
"Warning: invPreorder was deprecated in v2.0.
Please use converse-preorder instead."
#-}