Add Raw bundles to Relation.Binary.* hierarchy

[jamesmckinna]

This addresses the Relation.Binary.Bundles.Raw part of #2274 ahead of any subsequent refactoring of the Algebra hierarchy in earnest, to exploit the standardisation of vocabulary/fixity envisaged there.

Adds:

• RawX bundles systematically to mirror those in Relation.Binary.Bundles.X
• rawX manifest fields to each of those in Relation.Binary.Bundles.X

NB. Possible issues:

• By contrast with the main Relation.Bundles definitions, this introduces rawSetoid fields at the top level to each RawX bundle, in order to also introduce the negated equality symbol _≉_ uniformly.
• The DecX hierarchy is not mirrored with a parallel RawDecX hierarchy... which might otherwise violate the proposed alternative dependency structure outlined in [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252 .
• In the spirit of [DRY] why is _≉_ defined both for Algebra.Bundles.Raw.RawX bundles, and via Setoid instances, for Algebra.Bundles.X? #2274 the current design for ApartnessRelation introduces its negated relation symbol in the Structures hierarchy (cf. Algebra.Structures.IsGroup...), moreover without any fixity declaration; so there are/might be opportunities to rectify this design via public re-export...?

[Taneb]

This looks pretty good, but I do think that the changes to Relation.Binary.Bundles to export these should happen in this PR

[jamesmckinna]

UPDATED: Please ignore this comment!

The latest round of debugging commits suggest that the Eq submodules of Reation.Binary.Bundles.X seem to exist solely to play the 'helper' role envisaged by @JacquesCarette in exporting an extended signature for Setoids with the negated equality symbol... so a 'natural' further refactoring would be to remove all this Eq indirection completely? (At the cost of reifying my difference of opinion with Jacques...).

I'm not clear about the history of these things, but why do we have the Eq submodules factored out in this way? UPDATED: oh, I see that it's one way to ensure that refl and trans as field names don't clash between the underlying isEquivalence and the corresponding IsPreorder properties. I wonder if that was the good/better/best design choice, in favour of having fields names ≲-refl, ≲-trans etc.? Qualified names... hmmm.

[jamesmckinna]

This looks pretty good, but I do think that the changes to Relation.Binary.Bundles to export these should happen in this PR

Now added, and manifest at the top updated to reflect those additions.

[JacquesCarette]

git blame on Relation.Binary.Bundles tells me the first appearance of such a module Eq dates from September 2019 by @MatthewDaggitt back when the file was Relation.Binary.Packages in commit 7e00c92.

[JacquesCarette]

I'm somewhat undecided if this is the right thing to do. The code seems fine. It is definitely more consistent with what has been done elsewhere, so as a default, this is moving in a coherent direction. I'm just not quite ready to 'approve'.

[jamesmckinna]

@JacquesCarette writes:

I'm somewhat undecided if this is the right thing to do. The code seems fine. It is definitely more consistent with what has been done elsewhere, so as a default, this is moving in a coherent direction. I'm just not quite ready to 'approve'.

Beyond your comments on the originating issue #2274 can you say (more) about why you are/might be hesitating? (UPDATED: have just seen your more recent comment there... interesting!)

[JacquesCarette]

Teaching with PLFA right now, have updated to agda-2.7 and stdlib-2.2, and some things have gotten worse. I've got some issues to bring up when I have the time. One example: having Irrelevant show up in some of the goals when working on some stuff to do with Negation was unexpected and unwelcome. There's more.

[jamesmckinna]

Teaching with PLFA right now, have updated to agda-2.7 and stdlib-2.2, and some things have gotten worse. I've got some issues to bring up when I have the time. One example: having Irrelevant show up in some of the goals when working on some stuff to do with Negation was unexpected and unwelcome. There's more.

Are these issues to do with this PR, or general comments deserving a separate issue for v2.1/v2.2, or even on the PLFA tracker? hard to see how Relation.Nullary.Irrelevant might show up, except via Relation.Nullary.Negation.Core, other than... that should have happened before v2.0...? Shoutout also to @wenkokke who curates PLFA/agda/agda-stdlib compatibility...

[JacquesCarette]

Are these issues to do with this PR, or general comments deserving a separate issue for v2.1/v2.2,

The example is of the latter kind. But the reason I'm hesitating is related to me finding teaching with post-v2.0 stdlib a bit awkward compared to 1.7.

[jamesmckinna]

Are these issues to do with this PR, or general comments deserving a separate issue for v2.1/v2.2,

The example is of the latter kind. But the reason I'm hesitating is related to me finding teaching with post-v2.0 stdlib a bit awkward compared to 1.7.

Still: suggest you move this thread off this PR?

[wenkokke]

Are these issues to do with this PR, or general comments deserving a separate issue for v2.1/v2.2,

The example is of the latter kind. But the reason I'm hesitating is related to me finding teaching with post-v2.0 stdlib a bit awkward compared to 1.7.

Could you submit this as a separate issue, so that we can discuss these issues in detail?

[JacquesCarette]

@wenkokke wrote:

Could you submit this as a separate issue, so that we can discuss these issues in detail?

planning to! I've been swamped, so this is still in my ToDo queue.

[MatthewDaggitt]

I'm not clear about the history of these things, but why do we have the Eq submodules factored out in this way? UPDATED: oh, I see that it's one way to ensure that refl and trans as field names don't clash between the underlying isEquivalence and the corresponding IsPreorder properties. I wonder if that was the good/better/best design choice, in favour of having fields names ≲-refl, ≲-trans etc.? Qualified names... hmmm.

Yes, in retrospect it wasn't the best idea, but at the time, it was the only way to add them that preserved backwards compatibility.

[MatthewDaggitt]

The other refactorings look good though!

[MatthewDaggitt]

Hmm so following the pattern of Algebra.Bundles.Raw, then bundle equivalence is determined not by the names of the relation, but by their signature. For example both CommutativeMonoid and Monoid both have a single RawMonoid base.

Therefore to be consistent I think RawPreorder, RawPartialOrder, RawStrictPartialOrder and RawApartness relation should all be a single record... With what name I don't know...

If the purpose of this is to introduce syntax, then I think we need to use some other mechanism other than Raw bundles...

[jamesmckinna]

Two things:

• good point about shared signatures (and _∼_ would be the 'canonical' choice of symbol here?), and then let the corresponding Rawsub bundles in Bundles handle the renaming to orthodox/rectified syntax?
• as with discussions with @JacquesCarette , for me the issue is one of being able, for a given raw signature, to enrich it with 'obvious' derived operations which allow smoother treatment of subsequent properties etc. The 'syntax' aspect here is really about standardising notation for these otherwise useful/important derived notions...?

[jamesmckinna]

Latest commit introduces RawRelation in Relation.Binary.Bundles.Raw and associated rawRelation fields in Relation.Binary.Bundles, together with all the relevant hiding/renaming directives to fix the syntax.

Is this an improvement?

[jamesmckinna]

So, while I would still be happy/happier to see this merged (despite @JacquesCarette 's hesitation about doing so), it's somewhat ironic that we seem, via this route, to have reinstated the 'old' vocabulary (and then erased it via renaming... ;-)), cf. #2099 and its precursor issues/PRs. But I think that each time I/we go round this merry-go-round, things do actually improve?