Skip to content

[ add ] Relation.Binary.Properties.PartialSetoid #2678

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

Merged
merged 3 commits into from
Jun 17, 2025
Merged

[ add ] Relation.Binary.Properties.PartialSetoid #2678

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a5a5bd2
add: properties of PERs
jamesmckinna Mar 17, 2025
f5d35af
use: `Relation.Binary.Definitions`
jamesmckinna Mar 27, 2025
4095af1
make prefix `partial-`
jamesmckinna May 27, 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 @@ -120,6 +120,8 @@ New modules

* `Data.Sign.Show` to show a sign

* `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER

Additions to existing modules
-----------------------------

Expand Down
46 changes: 46 additions & 0 deletions src/Relation/Binary/Properties/PartialSetoid.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
------------------------------------------------------------------------
-- The Agda standard library
--
-- Additional properties for setoids
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Bundles using (PartialSetoid)

module Relation.Binary.Properties.PartialSetoid
{a ℓ} (S : PartialSetoid a ℓ) where

open import Data.Product.Base using (_,_; _×_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

open PartialSetoid S

private
variable
x y z : Carrier

------------------------------------------------------------------------
-- Proofs for partial equivalence relations

trans-reflˡ : x ≡ y → y ≈ z → x ≈ z
trans-reflˡ ≡.refl p = p
Copy link
Contributor

Choose a reason for hiding this comment

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

Do we actually need to match on the proof here? Is this not just a variant of subst?

Copy link
Contributor Author

@jamesmckinna jamesmckinna May 27, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Oh... yes, probably! er, no, actually, as the arguments are in the wrong order, and introducing a flip/≡.sym seemed like an indirection too far!?


trans-reflʳ : x ≈ y → y ≡ z → x ≈ z
trans-reflʳ p ≡.refl = p

p-reflˡ : x ≈ y → x ≈ x
p-reflˡ p = trans p (sym p)

p-reflʳ : x ≈ y → y ≈ y
p-reflʳ p = trans (sym p) p

p-refl : x ≈ y → x ≈ x × y ≈ y
p-refl p = p-reflˡ p , p-reflʳ p

p-reflexiveˡ : x ≈ y → x ≡ z → x ≈ z
Copy link
Contributor

Choose a reason for hiding this comment

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

This is Trans _≈_ _≡_ _≈_ (and similarly below), suggesting that reflexive may not be quite the right name? Similarly is this not just a variant of subst?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Hmmm... I see what you mean... Will ponder this for a bit!

Copy link
Contributor Author

@jamesmckinna jamesmckinna May 27, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

So... my reasoning (with a bit of post hoc rationalisation...) was as follows:

  • reflexive proofs are of the form x ≡ z → x ≈ z
  • these ones are 'partial', because preconditioned on having a proof of x ≈ y to licence them
  • the left/right designators then pick out which of x or y is being matched on

Possibly a bit convoluted, so I'm open to 'better' names!

Copy link
Contributor

Choose a reason for hiding this comment

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

This is not Trans _≈_ _≡_ _≈_ because the second x would be a y in that case.

This is an extremely weird property which basically says: if x is related to something (anything) and we have evidence of that, and x and z are identical, then we can get evidence that x and z are related.

I'm at a loss for what to name it.

Copy link
Contributor Author

@jamesmckinna jamesmckinna May 28, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I don't know about 'weird'... these properties are characteristic of being a PER rather than a full IsEquivalence!? Namely that the relation is reflexive only on its domain of definition, rather than on the whole type...

Copy link
Contributor Author

@jamesmckinna jamesmckinna May 29, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

As to names: I could call it (something like) conditional-reflexive, but then we would lose that the ≡.refl instantiation of such a lemma should be partial-refl... so those lemmas would also need to be renamed. And then... names are getting too long?

Copy link
Contributor

Choose a reason for hiding this comment

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

Weird likely because I generically find PERs weird.

However, your comment hits the real issue on the head: only on its domain of definition. We really ought to define an 'is defined' construction (a la Trans and Symmetric, etc) and use it here. Then I would have understood that you were asking for some indirect evidence of being defined. Then we'll be in a decent position to think about names.

At least now I understand this combinator's meaning (when x is defined, then equality that involve it is reflexive), and that is no longer weird at all.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Not sure I see clearly what the IsDefined construction would look like, and whether it would be 'free-standing', or tied to being in a PER?

Cf. Scott's "Identity and Existence in Intuitionistic Logic" (LNM 753) which explores variations on the theme of E t vs. t = t as expressions of 't is defined'/'t exists', but does seem tied to _=_ being an 'equality' (Leibniz-like) relation...?

p-reflexiveˡ p ≡.refl = p-reflˡ p

p-reflexiveʳ : x ≈ y → y ≡ z → y ≈ z
p-reflexiveʳ p ≡.refl = p-reflʳ p