diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5b3079dee4..37e11b619a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -88,3 +88,14 @@ Additions to existing modules
 
 * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
   be used infix.
+
+* In `Relation.Binary.Structures.IsPartialEquivalence`, added
+  commonly occurring derived combinations of `trans` and `sym`:
+  ```agda
+  infixr 5 _ᵒ⊗_ _⊗ᵒ_
+  transᵒ : RightTrans _≈_ (flip _≈_)
+  _⊗ᵒ_ = transᵒ
+  ᵒtrans : Trans (flip _≈_) _≈_  _≈_
+  _ᵒ⊗_ = ᵒtrans
+  ```
+
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 0dc5187228..4d7c57021d 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -16,9 +16,10 @@ module Relation.Binary.Structures
   where
 
 open import Data.Product.Base using (proj₁; proj₂; _,_)
+open import Function.Base using (flip)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Consequences
 open import Relation.Binary.Definitions
 
@@ -33,15 +34,26 @@ private
 -- as a module parameter at the top of this file.
 
 record IsPartialEquivalence : Set (a ⊔ ℓ) where
+  infixr 5 _ᵒ⊗_ _⊗ᵒ_
   field
     sym   : Symmetric _≈_
     trans : Transitive _≈_
 
+  transᵒ : RightTrans _≈_ (flip _≈_)
+  transᵒ eq₁ eq₂ = trans eq₁ (sym eq₂)
+
+  _⊗ᵒ_ = transᵒ
+
+  ᵒtrans : Trans (flip _≈_) _≈_  _≈_
+  ᵒtrans eq₁ eq₂ = trans (sym eq₁) eq₂
+
+  _ᵒ⊗_ = ᵒtrans
+
 -- The preorders of this library are defined in terms of an underlying
 -- equivalence relation, and hence equivalence relations are not
 -- defined in terms of preorders.
 
--- To preserve backwards compatability, equivalence relations are
+-- To preserve backwards compatibility, equivalence relations are
 -- not defined in terms of their partial counterparts.
 
 record IsEquivalence : Set (a ⊔ ℓ) where
@@ -51,7 +63,7 @@ record IsEquivalence : Set (a ⊔ ℓ) where
     trans : Transitive _≈_
 
   reflexive : _≡_ ⇒ _≈_
-  reflexive P.refl = refl
+  reflexive ≡.refl = refl
 
   isPartialEquivalence : IsPartialEquivalence
   isPartialEquivalence = record
@@ -59,6 +71,8 @@ record IsEquivalence : Set (a ⊔ ℓ) where
     ; trans = trans
     }
 
+  open IsPartialEquivalence isPartialEquivalence public
+    using (transᵒ; ᵒtrans; _ᵒ⊗_; _⊗ᵒ_)
 
 record IsDecEquivalence : Set (a ⊔ ℓ) where
   infix 4 _≟_