    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Convenient syntax for reasoning with a partial setoid
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (PartialSetoid)

    module Relation.Binary.Reasoning.PartialSetoid
      {s₁ s₂} (S : PartialSetoid s₁ s₂) where

    open import Relation.Binary.Reasoning.Syntax

    open PartialSetoid S

    import Relation.Binary.Reasoning.Base.Partial _≈_ trans
      as ≈-Reasoning

    ------------------------------------------------------------------------
    -- Reasoning combinators

    -- Export the combinators for partial relation reasoning, hiding the
    -- single misnamed combinator.
    open ≈-Reasoning public hiding (step-∼)

    -- Re-export the equality-based combinators instead
    open ≈-syntax _IsRelatedTo_ _IsRelatedTo_ ≈-Reasoning.∼-go sym public