From a5a5bd239d3aa65d79d742a754e604e2de29fb06 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 17 Mar 2025 10:46:49 +0000
Subject: [PATCH 1/2] add: properties of PERs

---
 CHANGELOG.md                                  |  2 +
 .../Binary/Properties/PartialSetoid.agda      | 46 +++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 src/Relation/Binary/Properties/PartialSetoid.agda

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..f81fb140a8
--- /dev/null
+++ b/src/Relation/Binary/Properties/PartialSetoid.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- 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.PropositionalEquality.Core as ≡ using (_≡_)
+
+open PartialSetoid S
+
+private
+  variable
+    x y z : Carrier
+
+------------------------------------------------------------------------
+-- Proofs for partial equivalence relations
+
+trans-reflˡ : x ≡ y → y ≈ z → x ≈ z
+trans-reflˡ ≡.refl p = p
+
+trans-reflʳ : x ≈ y → y ≡ z → x ≈ z
+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
+

From f5d35af05df2e4596b72f3ee53b701bf1fe5838e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 27 Mar 2025 07:48:50 +0000
Subject: [PATCH 2/2] use: `Relation.Binary.Definitions`

---
 src/Relation/Binary/Properties/PartialSetoid.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Binary/Properties/PartialSetoid.agda b/src/Relation/Binary/Properties/PartialSetoid.agda
index f81fb140a8..c2a60f051a 100644
--- a/src/Relation/Binary/Properties/PartialSetoid.agda
+++ b/src/Relation/Binary/Properties/PartialSetoid.agda
@@ -12,6 +12,7 @@ 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
@@ -23,10 +24,10 @@ private
 ------------------------------------------------------------------------
 -- Proofs for partial equivalence relations
 
-trans-reflˡ : x ≡ y → y ≈ z → x ≈ z
+trans-reflˡ : LeftTrans _≡_ _≈_
 trans-reflˡ ≡.refl p = p
 
-trans-reflʳ : x ≈ y → y ≡ z → x ≈ z
+trans-reflʳ : RightTrans _≈_ _≡_
 trans-reflʳ p ≡.refl = p
 
 p-reflˡ : x ≈ y → x ≈ x