Drop IsMagma from IsRawMagmaMorphism

[mwageringel]

I was a bit surprised to see that IsRawMagmaMorphism requires arguments of type IsMagma for domain and codomain, effectively making them not raw at all. Here is a proposal for dropping these parameters.

IsRawMagmaMorphism is mainly used in Algebra.Morphism.RawMagma to translate properties from the codomain to the domain assuming injectivity. There one needs to know that the codomain is a magma, but for the domain it follows by injectivity. Hence, I changed the To to be a Magma instead of a RawMagma.

Algebra.Morphism.RawMonoid is a bit awkward now as the codomain needs to be both a magma and a RawMonoid. I added an additional module parameter IsMagma for this.

Please let me know if this makes sense and if there is anything that could be improved.

[MatthewDaggitt]

I completely agree that the IsRawMagmaMorphism is a little bit misleading currently. I designed them like that as I couldn't personally come up with a use case where you could do any useful reasoning without the equality axioms. I assume that as you want to make this change you've got such a use case?

I've always had a sneaking suspicion that the RawX modules should have equality axioms included, and I'm wondering if that is the fundamental problem... I include them in my own Raw modules in my own library and they're certainly much more useful.

[mwageringel]

I am afraid I cannot think of a use case for raw magma morphisms without equality axioms either. I was thinking purely in terms of Algebra.Morphism.RawMagma and how it could be used to derive properties about subsets of algebraic structures, such as even integers or positive rationals. In these examples, with the PR one would automatically get a proof of IsMagma for the domain – although of course I have to admit it would not be hard to prove this manually. Perhaps, I should just add a helper function for this instead?

In order to make IsRawMagmaMorphism a bit less misleading, maybe it could be renamed to IsMagmaMorphism with F and T of type Magma? This would be equivalent to the current definition, as far as I can tell.

[MatthewDaggitt]

In order to make IsRawMagmaMorphism a bit less misleading, maybe it could be renamed to IsMagmaMorphism with F and T of type Magma? This would be equivalent to the current definition, as far as I can tell.

I agree that would seem to be the best option. The problem is that then, without RawMonoids having the equality axioms built in, then there is no obvious extension of that definition to IsRawMonoidMorphism... This would of course be fixed if we added the equality axioms to the Raw structures.

I am afraid I cannot think of a use case for raw magma morphisms without equality axioms either.

I'll ask on the Agda mailing list if anyone has a use case. If no-one has then I think the best thing to do is to adjust the definition of RawX. Obviously then RawMagma and Magma become indistinguishable and we get back to your definition 👍

[MatthewDaggitt]

Closed in favour of #958