Skip to content

[ add ] Setoid from PartialSetoid #2816

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 12 commits into
base: master
Choose a base branch
from
Draft

[ add ] Setoid from PartialSetoid #2816

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
f787fec
[ add ] `Setoid` from `PartialSetoid`
jamesmckinna Aug 22, 2025
51c0b54
fix: `CHANGELOG`
jamesmckinna Aug 24, 2025
a6144ca
restore: `Properties`
jamesmckinna Aug 28, 2025
bbdbe2b
restore: `Properties`
jamesmckinna Aug 28, 2025
324c197
fix: `CHANGELOG`
jamesmckinna Aug 28, 2025
3f73a0b
add: `Construct` module
jamesmckinna Aug 28, 2025
84a43af
refactor: use `proj₁` and `proj₂`
jamesmckinna Aug 29, 2025
80b3a4b
refactor: removed `refl` and inlined its definition
jamesmckinna Aug 29, 2025
cda4a4f
refactor: use `record` type
jamesmckinna Sep 1, 2025
fb73572
add: `Defined`
jamesmckinna Sep 1, 2025
97d6137
use: `Defined`
jamesmckinna Sep 1, 2025
f38d5b5
refactor: via `Kernel` pairs
jamesmckinna Sep 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
-----------------------------

Expand Down
61 changes: 61 additions & 0 deletions src/Relation/Binary/Construct/SetoidFromPartialSetoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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₁; proj₂)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know if it would be worse, or better, to have something like

Suggested change
open import Data.Product.Base using (_,_; Σ; proj₁; proj₂)
open import Data.Product.Base using (_,_; Σ)
renaming (proj₁ to ι; proj₂ to x≈x)

so that subsequent definitions can exploit such 'abstract' vocabulary/notation, rather than expose the concrete projection names?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Or perhaps better still, remove/inline refl as below, and make

ι : Carrier → S.Carrier
ι = proj₁

so that it may subsequently be exported/exportable as such?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you're going to go that route (second suggestion), why not bite the bullet and make the thing a record? Post-facto adding aliases for projections is what agda-unimath does... and it eventually leads to unreadable goals.

I like the first suggestion even less.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, in a way, the record-based version is (arguably) cleaner:

record SubSetoid : Set (a ⊔ ℓ) where

  field
    ι    : S.Carrier
    refl : ι S.≈ ι

open SubSetoid public using (ι)

_≈_ : Rel SubSetoid _
_≈_ = S._≈_ on ι

-- Structure

isEquivalence : IsEquivalence _≈_
isEquivalence = record
  { refl = λ {x = x} → SubSetoid.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 }

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I certainly would argue so!

Copy link
Contributor Author

@jamesmckinna jamesmckinna Aug 31, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the interests of clarity: are you saying that you would prefer that it be changed in favour of the record version?

More than happy to do so if so!

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done. I've retained Carrier as the name of the underlying type, but I suppose something else, such as SubSetoid, would work as well. Field name refl is kept hidden, so that its 'rectification' (wrt implicit quantification) as Setoid.refl is the way to access it.

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
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 _
_≈_ = S._≈_ on proj₁

-- Properties

refl : Reflexive _≈_
refl {x = x} = proj₂ 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 }