Add bundled homomorphisms #2383
Conversation
|
Before I look at this at all I just want to say thanks for tackling it! I've been avoiding it with the hope that we can get a solution for #2287, but that looks a long way off. |
|
@Taneb Indeed! This kind of boilerplate-bashing is quite fatiguing, until you run up against the 'diamond' re-export problem, at which point my powers fail me in different ways, trying to work out what should get re-exported from where... plus discovering that (still!) not everything is present which perhaps ought to be... ;-) UPDATED: moving to |
|
@JacquesCarette @Taneb I have now added the 'missing' parts of the PR (as in the revised opening preamble above), and so (hopefully) now stopping there... |
There was a problem hiding this comment.
The following don't need changes now but we should make issues for them so we don't lose track:
- Bundles for monomorphisms and isomorphisms (and epimorphisms if we add those) Add bundled mono-/iso-{/epi-} morphisms #2387
- Bundles for lattice-like and module-like morphisms Add bundles for lattice-like and module-like morphisms #2388
|
So I think that I now have added all the relevant (requested!) sub-{structure|bundle}s, but definitely needs another pass to check, along perhaps with a downstream issue/PR to fill in yet more gaps (including in the |
|
Thanks @JacquesCarette ! (modulo the need for manual effort in the absence of a Drasil-based solution...) |
src/Algebra/Morphism/Bundles.agda
Outdated
| -- Morphisms between Magmas | ||
| ------------------------------------------------------------------------ | ||
|
|
||
| record MagmaHomomorphism (A : Magma a ℓa) (B : Magma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where |
There was a problem hiding this comment.
Could you add a brief comment documenting why you decided to use Bundles here instead of the RawBundles used by the morphism structures? Having thought about it for all of a minute, it's not terribly obvious to me why we should make the switch. In particular, these morphisms are often used to transfer properties from one structure, e.g. a magma, to prove that another structure is also a magma. Assuming that they're both a magma to starts with, prevents you from using these morphisms for that purpose.
There was a problem hiding this comment.
Oh-ho-ho! Good catch... will have to go back to the drawing board and scratch my head for a bit.
My first (worst?) thought is that such a use case could be handled via the already-existing IsMagmaHomomorphism infrastructure... but I have not tested that conjecture (related to @Taneb 's #2276 on Monomorphisms?)... while the specific PR (#1962 ) which gave rise to (the use case giving rise to) this PR does already have the two Magma bundles at hand... and I'd never reconsidered that state of affairs...
There was a problem hiding this comment.
So yes, it can (and is!) handled by IsMagmaHomomorphism and co. The question is what does making them Bundles instead of RawBundles actually gains us? I can only see downsides.
There was a problem hiding this comment.
I think I'm convinced: but there's a knock-on consequence... : we can no longer define a SetoidHomomorphism manifest field at the bottom of the hierarchy... and probably Relation.Morphism.Bundles should be refactored to reflect (the eventual introduction of) RawSetoid as index for SetoidHomomorphism... ;-) cf. your #1464 / commit 9816023
There was a problem hiding this comment.
More knock-on:
- For
Algebra.Morphism.Construct.Identity, we needreflforIsXHomomorphism, so do we parametrise byxHomomorphismby the fullXbundle, or theRawXbundle, with an explicitreflwitness...? - Ditto. with
transforAlgebra.Morphism.Construct.Composition...
Advice welcome!
There was a problem hiding this comment.
Latest commits:
RawXbundle for the definitionXbundle for theConstructions
|
Currently badged as v2.2, but could merge for v2.1? |
Cherry-picked and enhanced from #1962 . Fixes #1960 .
TODO:
Algebra.Morphism.Construct.{Identity|Composition}materialRingWithoutOnedoesn't appear to export its ownRawsubstructure, so that should be added? ditto.KleeneAlgebraStructures/BundlesNB
Setoidstructure onHoms at all... (brain-fade; sigh)SemiringandRinghomomorphisms should export aSuccessorSetHomomorphismstructure/bundleonly after going back to Literals for any ring? #1363 through the medium of (the initial)
SuccessorSetand its consequences forAlgebra.Structureshaving(Is)SuccessorSetfields...