    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Convenient syntax for "equational reasoning" using a preorder
    ------------------------------------------------------------------------

    -- Example uses:
    --
    --    u∼y : u ∼ y
    --    u∼y = begin
    --      u  ≈⟨ u≈v ⟩
    --      v  ≡⟨ v≡w ⟩
    --      w  ∼⟨ w∼y ⟩
    --      y  ≈⟨ z≈y ⟩
    --      z  ∎
    --
    --    u≈w : u ≈ w
    --    u≈w = begin-equality
    --      u  ≈⟨ u≈v ⟩
    --      v  ≡⟨ v≡w ⟩
    --      w  ≡⟨ x≡w ⟨
    --      x  ∎

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

    open import Relation.Binary.Bundles using (Preorder)

    module Relation.Binary.Reasoning.Preorder
      {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where

    open Preorder P

    ------------------------------------------------------------------------
    -- Publicly re-export the contents of the base module

    open import Relation.Binary.Reasoning.Base.Double isPreorder public