Sandro Stucki
Sandro Stucki
> Given that, can we wait to see how the discussion around the proposal plays out? Absolutely. I am not in a rush with this one. I think the contents...
Shout-out to @Taneb who originally suggested implementing this PR.
> @sstucki just doing this now. The first thing I notice is that the fields of `IsSemiring` and `IsPosemiring` are not symmetric? Is there a reason why not? Sorry @MatthewDaggitt,...
> I'd expect it to be: > > ```agda > record IsPosemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where >...
> The problem is that if it was added then the record definition of `IsPosemiring` couldn't be updated in a backwards compatible manner. I don't understand what you mean by...
BTW, if you want me to "fill in" the missing structures in the `Algebra.Ordered` hierarchy for the sake of symmetry, I don't mind doing that. I'm less eager to add...
Thanks for the nice diagrams @MatthewDaggitt, they are very helpful. But I don't entirely buy it. You say > Here, if the base `Algebra.Structures` hierarchy changes, then nothing needs to...
> > Also, code that depends on the base hierarchy still breaks if that changes. > > That's the thing though, yes the code in the library breaks and yes...
> Would you be willing to change it? I Yes. But it may take a while (I have some other obligations this week), sorry. If it's urgent, please go ahead...
I like the idea, but boy is it going to break backwards compatibility! 😉 That being said, I think people are generally used to the library being in flux at...