Reconciling the indices of `IsX` with those of the corresponding `RawX` about agda-stdlib HOT 5 OPEN

I've also wondered about this from time to time, and I think it's mainly a swings and roundabouts issues. As you say, one of advantages is that you can import Structures while fixing the equality. This a feature that we use relatively widely in the library.

I agree with @JacquesCarette's points as well that this may be a language design question.

If no one objects, then I might add this to the hypothetical-rewrite milestone.

from agda-stdlib.

This is yet another form of the eternal bundled / unbundled question. The correct answer is: don't choose, they are equivalent. Pragmatically, that remains a non-answer because, in Agda, this equivalence can only be witnessed tediously on a case-by-case basis.

Unfortunately, I have no idea what the actual ergonomics of each choice is. This would need a great big (costly) experiment, and it doesn't seem to me that we can decide this just as a thought experiment.

In theory, I personally like to group things together more. But that's at the "gut feel" level rather than at the "let's make this the design NOW" level.

from agda-stdlib.

Well put, and so I guess I defer to your wise insight. Sigh... That said, if there were an agency willing to fund the costly experiment, ... or indeed, whether your remark is enough to encourage a zealot to pursue it for its own sake anyway... ;-) (best not, but the devil on my shoulder, etc.)

And... I don't think I was proposing it as THE design, but as with Algebra.*.Biased, as an alternative means to an end...

from agda-stdlib.

Well look at that, a hypothetical-rewrite milestone - very nice.

Hmm, I'd be tempted to start a page on the Wiki also collecting language changes that we library writers would really like to see.

from agda-stdlib.

One argument against punting this to the indefinite future with hypothetical-rewrite: the issue(s) arising from #2251 and #2268 : if we add derived operations to the Raw bundle (which makes sense from the point of view of them being 'raw' operations), then they don't get inherited in the IsStructure definition, only in the Bundled version. But if we index the Structure.IsX on the RawX bundle, then we get them 'for free'.
Similarly (a related, but distinct, issue): Algebra.Properties.X expects a Bundled X, instead of (more simply?) an instance of IsX... is this the 'correct' factorisation of the dependencies?

And the second: consistency/uniformity. We index homomorphisms between Structures.IsX and Bundles.X via their underlying RawX bundles, so 'on morphisms' we observe one discipline, but 'on objects' another... which seems an anomaly worth correcting.

from agda-stdlib.