mechvel

The fresh version (version 3) of the proposal had been lost somewhere in pull requests. For any occasion I upload it here: [onIntegralSemiring-3.zip](https://github.com/user-attachments/files/18547621/onIntegralSemiring-3.zip)

James, thank you for correcting the proposal. Is it possible to get the archive of the source of the pull request 3f6bdbb you have done? If it is possible, I...

James, please inform me when it appears a reasonable moment for me to download the library version (I hope I will be able to download the archive of the source)....

Taneb wrote > @mechvel, you can download an archive at that commit here: https://github.com/agda/agda-stdlib/archive > /3f6bdbb86b3c45f8eb1af8e9d042dac26893123f.zip > > I found this link by clicking the commit, pressing the "Browse files"...

@jamesmckinna asks > deprecate (Is)CancellativeCommutativeSemiring in favour of Integral versions? For `Ring`, I believe, these two are equivalent. So that `CancellativeRing` is not needed. But how do you derive ``Integral...

James wrote * fold definition of Trivial better into Algebra.Definitions so that Algebra.Definitions.Integral can make use of it? * breaking rephrase Algebra.Properties.Semiring.Primality in terms of Trivial? Is `Trivial` ever defined...

I wrote about trying to derive Integral ==> LeftCancellative for Semiring. Each S : Ring has the commutative additive Monoid M. M can be extended to A : AbeleanGroup (probably...

The definition of AlmostLeft(Right)Cancellative ``∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`` is given (by myself) several...

I think Taneb is right. ``` lemma1 : (1# ≈ 0# ⊎ NoZeroDivisors 0# _∙_) → NoZeroDivisors 0# _∙_ lemma1 (inj₁ 1≈0) = noZeroDivisors -- because everything equals zero due...

But I have lost the first archive that I uploaded to here. Can people find it on GitHub?