mechvel

Changing `_∣_` in Nat.Divisibiliy may break backwards compatibiliy greatly. At least the team could add the conversion that allows people to use generic `_∣_` and the ad-hoc one for Nat:...

Currently I use `Nat.Factorisation.factorise` with converting the result parts to the generic (standard) definitions of `Irreducible` and `Prime`. I hope that in lib-3.0 this conversion will not be necessary. But...

It is better to use above the names Irreducible-adHoc and Prime-adHoc with using `-adHoc` instead of `-std`. Because both versions are in Standard of lib-2.1-rc1, only one is ad-hoc for...

> the dependency graph: Data.List.Base and Properties need to import Data.Nat.Divisibility otherwise unnecessarily; also, > how much of Algebra should be imported by 'concrete' Data modules? Data.List.Properties ends up being...

> I emphatically agree with removing sum and product from Data.List.Base. In my proposal with IntegralSemiring, `product` and its properties for Nat are moved to Data/Nat/List.agda : the items for...

But there is a more general condition for ``map f xs ≋ map g ys``, which is widely used: ``` map-pointwise-≈ : {f g : A → B} {xs ys...

I wrote a certain erroneous message and have deleted it. Please, read this new one. I think now that the notice by James@jamesmckinna is important. I have missed the following...

James, thank you for your comments. I an surprised with that I have forgotten light-headedly of the difference between ``¬ A → B`` and ``A ⊎ B``. Now I revisit...

I think that the above "positive" approach to definitions of Field and IntegralSemiring accommodates them better to the needs of constructive algebra, because sometimes the equality is not decidable. On...

Please, find attached the improved version archive of the proposal. First see there Readme.lagda. [onIntegralSemiring.zip](https://github.com/user-attachments/files/18466487/onIntegralSemiring.zip)