Define IsUnitalMagma and IsQuasigroup

[Akshobhya1234]

• IsUnitalMagma
• IsQuasigroup

[MatthewDaggitt]

Hi @Akshobhya1234, thank you for the PR! Got a few comments:

1. These structures should go in the correct place in the file. Look for section headings -- Structures with 1 binary operation & 1 element and -- Structures with 1 binary operation, 1 unary operation & 1 element

2. You will also have to go through all the larger structures in the file (e.g. IsMonoid) and add the corresponding re-exports of IsUnitalSemigroup and IsQuasigroup. Unfortunately this process is quadratic in the number of structures in the file, and is a well-known problem which @JacquesCarette and others are working on.

3. You should add the bundled versions of them in Algebra.Bundles as well.

[MatthewDaggitt]

Oh and and you'll need to run fix-whitespace as described in HACKING.md

[MatthewDaggitt]

Hi @Akshobhya1234, maybe let's just stick with IsUnitalMagma and IsQuasigroup in this PR and try and get it merged in. We can then tackle IsLoop in a future PR.

I see that you have carried out points 1. and 3. from review, thanks! Do you know what to do for point 2.?

[Akshobhya1234]

Hi @Akshobhya1234, maybe let's just stick with IsUnitalMagma and IsQuasigroup in this PR and try and get it merged in. We can then tackle IsLoop in a future PR.

I see that you have carried out points 1. and 3. from review, thanks! Do you know what to do for point 2.?

Hi @MatthewDaggitt I am not sure about point 2. I will remove IsLoop for this PR.

[MatthewDaggitt]

@Akshobhya1234 apologies for the delay in replying. Had a paper deadline last week and this slipped off my radar.

What I mean by point 2. is that you will need to construct the new structures you've added in larger structures that contain those structures. For example, look at how IsCommutativeMonoid constructs IsCommutativeSemigroup because IsCommutativeMonoid inherits directly from IsMonoid.

agda-stdlib/src/Algebra/Structures.agda

Lines 129 to 138 in 28cdb06

	open IsMonoid isMonoid public
	isCommutativeSemigroup : IsCommutativeSemigroup ∙
	isCommutativeSemigroup = record
	{ isSemigroup = isSemigroup
	; comm = comm
	}
	open IsCommutativeSemigroup isCommutativeSemigroup public
	using (isCommutativeMagma)

In the same way you should make it so IsMonoid constructs an instance of IsUnitalMagma. You will then need to do suitable renaming in larger structures such as rings and semirings, + then go through bundles and do the same thing.

Does that make sense?

[Akshobhya1234]

@MatthewDaggitt Thank you for the specific example. I will look into it. However I see that it is indeed a quadratic problem. I will try to come up with something at the earliest.

[JacquesCarette]

I don't really have additional comments beyond @MatthewDaggitt -- when are you going to complete the changes that were asked?

[Akshobhya1234]

I don't really have additional comments beyond @MatthewDaggitt -- when are you going to complete the changes that were asked?

@JacquesCarette apologies for the delay. I will try and complete it by next week.

[Akshobhya1234]

@MatthewDaggitt Kindly let me know if I am missing something. If I open isUnitalMagma in IsMonoid using isMagma, then, in MonoidMonomorphism I get this error

"Cannot resolve overloaded projection isMagma because it is not applied to a visible argument when checking that the expression M.isMagma has type IsMagma ≈₂ ◦"

So I didn't do it as it will fail the make test.

[MatthewDaggitt]

Thanks, that looks good! I've made a few minor tweaks, and if the tests pass then I'll merge it in.

If I open isUnitalMagma in IsMonoid using isMagma, then, in MonoidMonomorphism I get this error

Yes, you don't want to reopen IsUnitalMagma fully because, as you found, it contains definitions that are already in scope from opening IsSemigroup.

[MatthewDaggitt]

Tests are passing so merging in! Thanks for the PR @Akshobhya1234, sorry it's taken so long. Hopefully we'll get any future ones you make merged in quicker.