diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76e6a12c76..93fa29b37b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -120,6 +120,8 @@ New modules
 
 * `Data.Sign.Show` to show a sign
 
+* `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER
+
 Additions to existing modules
 -----------------------------
 
diff --git a/src/Relation/Binary/Properties/PartialSetoid.agda b/src/Relation/Binary/Properties/PartialSetoid.agda
new file mode 100644
index 0000000000..c2a60f051a
--- /dev/null
+++ b/src/Relation/Binary/Properties/PartialSetoid.agda
@@ -0,0 +1,47 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Additional properties for setoids
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (PartialSetoid)
+
+module Relation.Binary.Properties.PartialSetoid
+  {a ℓ} (S : PartialSetoid a ℓ) where
+
+open import Data.Product.Base using (_,_; _×_)
+open import Relation.Binary.Definitions using (LeftTrans; RightTrans)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+
+open PartialSetoid S
+
+private
+  variable
+    x y z : Carrier
+
+------------------------------------------------------------------------
+-- Proofs for partial equivalence relations
+
+trans-reflˡ : LeftTrans _≡_ _≈_
+trans-reflˡ ≡.refl p = p
+
+trans-reflʳ : RightTrans _≈_ _≡_
+trans-reflʳ p ≡.refl = p
+
+p-reflˡ : x ≈ y → x ≈ x
+p-reflˡ p = trans p (sym p)
+
+p-reflʳ : x ≈ y → y ≈ y
+p-reflʳ p = trans (sym p) p
+
+p-refl : x ≈ y → x ≈ x × y ≈ y
+p-refl p = p-reflˡ p , p-reflʳ p
+
+p-reflexiveˡ : x ≈ y → x ≡ z → x ≈ z
+p-reflexiveˡ p ≡.refl = p-reflˡ p
+
+p-reflexiveʳ : x ≈ y → y ≡ z → y ≈ z
+p-reflexiveʳ p ≡.refl = p-reflʳ p
+