[ 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,6 +101,11 @@ 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.Definitions`
+  ```agda
+  Defined : Rel A ℓ → A → Set ℓ
+  ```
+
 * In `Relation.Nullary.Negation.Core`
   ```agda
   ¬¬-η : A → ¬ ¬ A

src/Relation/Binary/Construct/Kernel.agda

@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Equaliser of a kernel pair in Setoid
+------------------------------------------------------------------------
+
+open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
+
+module Relation.Binary.Construct.Kernel
+  {a i ℓ} {I : Set i}
+  (S : PartialSetoid a ℓ) (let module S = PartialSetoid S)
+  (f g : I → S.Carrier)
+  where
+
+open import Function.Base using (id; _∘_; _on_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Defined)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
+
+import Relation.Binary.Properties.PartialSetoid S as Properties
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+record Carrier : Set (a ⊔ i ⊔ ℓ) where
+
+  field
+    h    : I
+    refl : (f h) S.≈ (g h)
+
+  ι : S.Carrier
+  ι = f h
+
+
+open Carrier public using (ι)
+
+_≈_ : Rel Carrier _
+_≈_ = S._≈_ on ι
+
+-- Structure
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record
+  { refl = λ {x = x} → Properties.partial-reflˡ (Carrier.refl x)
+  ; sym = S.sym
+  ; trans = S.trans
+  }
+
+-- Bundle
+
+setoid : Setoid _ _
+setoid = record { isEquivalence = isEquivalence }
+
+-- Monomorphism
+
+isRelHomomorphism : IsRelHomomorphism _≈_ S._≈_ ι
+isRelHomomorphism = record { cong = id }
+
+isRelMonomorphism : IsRelMonomorphism _≈_ S._≈_ ι
+isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = id }
+

src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda

@@ -0,0 +1,58 @@
+------------------------------------------------------------------------
+-- 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 Function.Base using (id; _on_)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Defined)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism)
+
+private
+  module S = PartialSetoid S
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+record Carrier : Set (a ⊔ ℓ) where
+
+  field
+    ι    : S.Carrier
+    refl : Defined S._≈_ ι
+
+open Carrier public using (ι)
+
+_≈_ : Rel Carrier _
+_≈_ = S._≈_ on ι
+
+-- Structure
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record
+  { refl = λ {x = x} → Carrier.refl x
+  ; sym = S.sym
+  ; trans = S.trans
+  }
+
+-- Bundle
+
+setoid : Setoid _ _
+setoid = record { isEquivalence = isEquivalence }
+
+-- Monomorphism
+
+isRelHomomorphism : IsRelHomomorphism _≈_ S._≈_ ι
+isRelHomomorphism = record { cong = id }
+
+isRelMonomorphism : IsRelMonomorphism _≈_ S._≈_ ι
+isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = id }

src/Relation/Binary/Construct/SubSetoid.agda

@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Conversion of a PartialSetoid into a Setoid
+------------------------------------------------------------------------
+
+open import Relation.Binary.Bundles using (PartialSetoid)
+
+module Relation.Binary.Construct.SubSetoid
+  {a ℓ} (S : PartialSetoid a ℓ)
+  where
+
+open import Function.Base using (id)
+import Relation.Binary.Construct.Kernel as Kernel
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+open module SubSetoid = Kernel S id id public

src/Relation/Binary/Definitions.agda

@@ -37,8 +37,11 @@ private
 -- e.g. in the definition of `IsEquivalence` later in this file. This
 -- convention is a legacy from the early days of the library.
 
+Defined : Rel A ℓ → A → Set ℓ
+Defined _∼_ x = x ∼ x
+
 Reflexive : Rel A ℓ → Set _
-Reflexive _∼_ = ∀ {x} → x ∼ x
+Reflexive _∼_ = ∀ {x} → Defined _∼_ x
 
 -- Generalised symmetry.