    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties satisfied by preorders
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (Preorder; Setoid)

    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
      using (isPreorder; preorder)
    open import Relation.Binary.Structures using (IsPreorder)

    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."
    #-}