[ add ] Setoid from PartialSetoid

CHANGELOG.md

@@ -48,6 +48,8 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
 
+* `Relation.Binary.Construct.SetoidFromPartialSetoid`.
+
 Additions to existing modules
 -----------------------------
 
@@ -99,17 +101,6 @@ 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/Construct/SetoidFromPartialSetoid.agda

@@ -0,0 +1,61 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Conversion of a PartialSetoid into a Setoid
+------------------------------------------------------------------------
+
+open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
+
+module Relation.Binary.Construct.SetoidFromPartialSetoid
+  {a ℓ} (S : PartialSetoid a ℓ) where
+
+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)
+open import Relation.Binary.Structures
+  using (IsPartialEquivalence; IsEquivalence)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
+
+private
+  module S = PartialSetoid S
+
+  variable
+    x y z : S.Carrier
+
+------------------------------------------------------------------------
+-- Definitions
+
+Carrier : Set _
+Carrier = Σ S.Carrier λ x → x S.≈ x
+
+_≈_ : Rel Carrier _
+x≈x@(x , _) ≈ y≈y@(y , _) = x S.≈ y
+
+-- Properties
+
+refl : Reflexive _≈_
+refl {x = _ , x≈x} = x≈x
+
+-- Structure
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record
+  { refl = λ {x} → refl {x = x}
+  ; sym = S.sym
+  ; trans = S.trans
+  }
+
+-- Bundle
+
+setoid : Setoid _ _
+setoid = record { isEquivalence = isEquivalence }
+
+-- Monomorphism
+
+isRelHomomorphism : IsRelHomomorphism _≈_ S._≈_ proj₁
+isRelHomomorphism = record { cong = id }
+
+isRelMonomorphism : IsRelMonomorphism _≈_ S._≈_ proj₁
+isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = id }

src/Relation/Binary/Properties/PartialSetoid.agda

@@ -6,29 +6,21 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
+open import Relation.Binary.Bundles using (PartialSetoid)
 
 module Relation.Binary.Properties.PartialSetoid
   {a ℓ} (S : PartialSetoid a ℓ) where
 
-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 Data.Product.Base using (_,_; _×_)
+open import Relation.Binary.Definitions using (LeftTrans; RightTrans)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-import Relation.Binary.Structures as Structures
-  using (IsPartialEquivalence; IsEquivalence)
-open import Relation.Binary.Morphism.Structures
-  using (IsRelHomomorphism; IsRelMonomorphism)
 
-private
-  open module PER = PartialSetoid S
+open PartialSetoid S
 
+private
   variable
     x y z : Carrier
 
-
 ------------------------------------------------------------------------
 -- Proofs for partial equivalence relations
 
@@ -53,37 +45,3 @@ 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 }
-