From f787feccb7829148e0ab94129907fd29a992372b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 22 Aug 2025 03:56:00 +0100 Subject: [PATCH 01/12] [ add ] `Setoid` from `PartialSetoid` --- .../Binary/Properties/PartialSetoid.agda | 52 +++++++++++++++++-- 1 file changed, 47 insertions(+), 5 deletions(-) diff --git a/src/Relation/Binary/Properties/PartialSetoid.agda b/src/Relation/Binary/Properties/PartialSetoid.agda index aac637718a..34c6b1ccf1 100644 --- a/src/Relation/Binary/Properties/PartialSetoid.agda +++ b/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 } + From 51c0b54b4ffd4f25ebcf2ed9e69a3a6f4fededb1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 24 Aug 2025 11:50:10 +0100 Subject: [PATCH 02/12] fix: `CHANGELOG` --- CHANGELOG.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..7c681c0439 100644 --- a/CHANGELOG.md +++ b/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 From a6144ca4caaf436a43dd435d191ef3f43f7924cd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Aug 2025 12:38:51 +0100 Subject: [PATCH 03/12] restore: `Properties` --- .../Binary/Properties/PartialSetoid.agda | 52 ++----------------- 1 file changed, 5 insertions(+), 47 deletions(-) diff --git a/src/Relation/Binary/Properties/PartialSetoid.agda b/src/Relation/Binary/Properties/PartialSetoid.agda index 34c6b1ccf1..47c0a0113c 100644 --- a/src/Relation/Binary/Properties/PartialSetoid.agda +++ b/src/Relation/Binary/Properties/PartialSetoid.agda @@ -6,25 +6,18 @@ {-# 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 @@ -52,38 +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 } - From bbdbe2be637559c810e7e3d37f9272c036acad65 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Aug 2025 12:39:36 +0100 Subject: [PATCH 04/12] restore: `Properties` --- src/Relation/Binary/Properties/PartialSetoid.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Properties/PartialSetoid.agda b/src/Relation/Binary/Properties/PartialSetoid.agda index 47c0a0113c..aac637718a 100644 --- a/src/Relation/Binary/Properties/PartialSetoid.agda +++ b/src/Relation/Binary/Properties/PartialSetoid.agda @@ -21,7 +21,6 @@ private variable x y z : Carrier - ------------------------------------------------------------------------ -- Proofs for partial equivalence relations @@ -45,3 +44,4 @@ partial-reflexiveˡ p ≡.refl = partial-reflˡ p partial-reflexiveʳ : x ≈ y → y ≡ z → y ≈ z partial-reflexiveʳ p ≡.refl = partial-reflʳ p + From 324c1975d4519855a9508e18160425d169be30ed Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Aug 2025 12:40:28 +0100 Subject: [PATCH 05/12] fix: `CHANGELOG` --- CHANGELOG.md | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c681c0439..9ee9911b58 100644 --- a/CHANGELOG.md +++ b/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 From 3f73a0bb86ae7f8a6102d9a6cd0537e648f9f222 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 28 Aug 2025 12:47:47 +0100 Subject: [PATCH 06/12] add: `Construct` module --- .../Construct/SetoidFromPartialSetoid.agda | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda diff --git a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda new file mode 100644 index 0000000000..7ec60b1751 --- /dev/null +++ b/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 } From 84a43afe979b83de47e7c83314d6695cd2d5bf60 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 29 Aug 2025 05:26:45 +0100 Subject: [PATCH 07/12] =?UTF-8?q?refactor:=20use=20`proj=E2=82=81`=20and?= =?UTF-8?q?=20`proj=E2=82=82`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Binary/Construct/SetoidFromPartialSetoid.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda index 7ec60b1751..5fc945f2d4 100644 --- a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda +++ b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda @@ -9,8 +9,8 @@ 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 Data.Product.Base using (_,_; Σ; proj₁; proj₂) +open import Function.Base using (id; _on_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Reflexive) open import Relation.Binary.Structures @@ -31,12 +31,12 @@ Carrier : Set _ Carrier = Σ S.Carrier λ x → x S.≈ x _≈_ : Rel Carrier _ -x≈x@(x , _) ≈ y≈y@(y , _) = x S.≈ y +_≈_ = S._≈_ on proj₁ -- Properties refl : Reflexive _≈_ -refl {x = _ , x≈x} = x≈x +refl {x = x} = proj₂ x -- Structure From 80b3a4b02a4b6eedb338f024ce6f22a473a3583f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 29 Aug 2025 16:11:07 +0100 Subject: [PATCH 08/12] refactor: removed `refl` and inlined its definition --- .../Binary/Construct/SetoidFromPartialSetoid.agda | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda index 5fc945f2d4..c242bc7797 100644 --- a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda +++ b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda @@ -12,7 +12,6 @@ module Relation.Binary.Construct.SetoidFromPartialSetoid open import Data.Product.Base using (_,_; Σ; proj₁; proj₂) open import Function.Base using (id; _on_) 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 @@ -33,16 +32,11 @@ Carrier = Σ S.Carrier λ x → x S.≈ x _≈_ : Rel Carrier _ _≈_ = S._≈_ on proj₁ --- Properties - -refl : Reflexive _≈_ -refl {x = x} = proj₂ x - -- Structure isEquivalence : IsEquivalence _≈_ isEquivalence = record - { refl = λ {x} → refl {x = x} + { refl = λ {x = x} → proj₂ x ; sym = S.sym ; trans = S.trans } From cda4a4f9456ebeedfca87156756e1a733abc92b4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 Sep 2025 05:28:31 +0100 Subject: [PATCH 09/12] refactor: use `record` type --- .../Construct/SetoidFromPartialSetoid.agda | 23 +++++++++++-------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda index c242bc7797..6432904706 100644 --- a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda +++ b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda @@ -9,34 +9,37 @@ 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₁; proj₂) open import Function.Base using (id; _on_) +open import Level using (_⊔_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Structures - using (IsPartialEquivalence; IsEquivalence) + using (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 +record Carrier : Set (a ⊔ ℓ) where + + field + ι : S.Carrier + refl : ι S.≈ ι + +open Carrier public using (ι) _≈_ : Rel Carrier _ -_≈_ = S._≈_ on proj₁ +_≈_ = S._≈_ on ι -- Structure isEquivalence : IsEquivalence _≈_ isEquivalence = record - { refl = λ {x = x} → proj₂ x + { refl = λ {x = x} → Carrier.refl x ; sym = S.sym ; trans = S.trans } @@ -48,8 +51,8 @@ setoid = record { isEquivalence = isEquivalence } -- Monomorphism -isRelHomomorphism : IsRelHomomorphism _≈_ S._≈_ proj₁ +isRelHomomorphism : IsRelHomomorphism _≈_ S._≈_ ι isRelHomomorphism = record { cong = id } -isRelMonomorphism : IsRelMonomorphism _≈_ S._≈_ proj₁ +isRelMonomorphism : IsRelMonomorphism _≈_ S._≈_ ι isRelMonomorphism = record { isHomomorphism = isRelHomomorphism ; injective = id } From fb735723b82619428d868f5ea0e11199635b5898 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 Sep 2025 14:42:04 +0100 Subject: [PATCH 10/12] add: `Defined` --- CHANGELOG.md | 5 +++++ src/Relation/Binary/Definitions.agda | 5 ++++- 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9ee9911b58..ed044a6bbc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -101,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 diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 80b9e5ff44..820b83b0db 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/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. From 97d61374cafa441b9290b23b9c8739573c3a3f7c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 1 Sep 2025 14:46:50 +0100 Subject: [PATCH 11/12] use: `Defined` --- src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda index 6432904706..2908e75cca 100644 --- a/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda +++ b/src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda @@ -12,8 +12,8 @@ module Relation.Binary.Construct.SetoidFromPartialSetoid open import Function.Base using (id; _on_) open import Level using (_⊔_) open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Structures - using (IsEquivalence) +open import Relation.Binary.Definitions using (Defined) +open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism; IsRelMonomorphism) @@ -28,7 +28,7 @@ record Carrier : Set (a ⊔ ℓ) where field ι : S.Carrier - refl : ι S.≈ ι + refl : Defined S._≈_ ι open Carrier public using (ι) From f38d5b54540f0fe10d8d7c152d533801c130a250 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 3 Sep 2025 09:13:22 +0100 Subject: [PATCH 12/12] refactor: via `Kernel` pairs --- src/Relation/Binary/Construct/Kernel.agda | 65 ++++++++++++++++++++ src/Relation/Binary/Construct/SubSetoid.agda | 20 ++++++ 2 files changed, 85 insertions(+) create mode 100644 src/Relation/Binary/Construct/Kernel.agda create mode 100644 src/Relation/Binary/Construct/SubSetoid.agda diff --git a/src/Relation/Binary/Construct/Kernel.agda b/src/Relation/Binary/Construct/Kernel.agda new file mode 100644 index 0000000000..0b90c780fc --- /dev/null +++ b/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 } + diff --git a/src/Relation/Binary/Construct/SubSetoid.agda b/src/Relation/Binary/Construct/SubSetoid.agda new file mode 100644 index 0000000000..abf7155bfe --- /dev/null +++ b/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