[ add ] Setoid from PartialSetoid

CHANGELOG.md

@@ -99,6 +99,17 @@ Additions to existing modules
                     updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ padRight m≤n x (updateAt xs i f)
   ```
 
+* In `Relation.Binary.Properties.PartialSetoid`
+  ```agda
+  Carrierₛ          : Set _
+  _≈ₛ_              : Rel Carrierₛ _
+  reflₛ             : Reflexive _≈ₛ_
+  isEquivalenceₛ    : IsEquivalence _≈ₛ_
+  setoidₛ           : Setoid _ _
+  isRelHomomorphism : IsRelHomomorphism _≈ₛ_ _≈_ proj₁
+  isRelMonomorphism : IsRelMonomorphism _≈ₛ_ _≈_ proj₁
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η : A → ¬ ¬ A

src/Relation/Binary/Properties/PartialSetoid.agda

@@ -6,21 +6,29 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Bundles using (PartialSetoid)
+open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
 
 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 Data.Product.Base using (_,_; _×_; Σ; proj₁)
+open import Function.Base using (id)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive; LeftTrans; RightTrans)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-
-open PartialSetoid S
+import Relation.Binary.Structures as Structures
+  using (IsPartialEquivalence; IsEquivalence)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
 
 private
+  open module PER = PartialSetoid S
+
   variable
     x y z : Carrier
 
+
 ------------------------------------------------------------------------
 -- Proofs for partial equivalence relations
 
@@ -45,3 +53,37 @@ partial-reflexiveˡ p ≡.refl = partial-reflˡ p
 partial-reflexiveʳ : x ≈ y → y ≡ z → y ≈ z
 partial-reflexiveʳ p ≡.refl = partial-reflʳ p
 
+------------------------------------------------------------------------
+-- Setoids from partial setoids
+
+-- Definitions
+
+Carrierₛ : Set _
+Carrierₛ = Σ Carrier λ x → x ≈ x
+
+_≈ₛ_ : Rel Carrierₛ _
+x≈x@(x , _) ≈ₛ y≈y@(y , _) = x ≈ y
+
+-- Properties
+
+reflₛ : Reflexive _≈ₛ_
+reflₛ {x = _ , x≈x} = x≈x
+
+-- Structure
+
+isEquivalenceₛ : Structures.IsEquivalence _≈ₛ_
+isEquivalenceₛ = record { refl = λ {x} → reflₛ {x = x} ; sym = sym ; trans = trans }
+
+-- Bundle
+
+setoidₛ : Setoid _ _
+setoidₛ = record { isEquivalence = isEquivalenceₛ }
+
+-- Monomorphism
+
+isRelHomomorphism : IsRelHomomorphism _≈ₛ_ _≈_ proj₁
+isRelHomomorphism = record { cong = id }
+
+isRelMonomorphism : IsRelMonomorphism _≈ₛ_ _≈_ proj₁
+isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = id }
+