Add derived (pre-)groupoid operations to Relation.Binary.Is(Partial)Equivalence

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
+  ```
+

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,14 +63,16 @@ record IsEquivalence : Set (a ⊔ ℓ) where
     trans : Transitive _≈_
 
   reflexive : _≡_ ⇒ _≈_
-  reflexive P.refl = refl
+  reflexive ≡.refl = refl
 
   isPartialEquivalence : IsPartialEquivalence
   isPartialEquivalence = record
     { sym = sym
     ; trans = trans
     }
 
+  open IsPartialEquivalence isPartialEquivalence public
+    using (transᵒ; ᵒtrans; _ᵒ⊗_; _⊗ᵒ_)
 
 record IsDecEquivalence : Set (a ⊔ ℓ) where
   infix 4 _≟_