Jacques Carette
Jacques Carette
Don't those result all follow from initiality and the two `from` functions being (rig/ring) homomorphisms? The one tricky one would be about `fromℕ′-∸` because that's not a "classical" operation that...
I agree with @jamesmckinna .
I really dislike that `Data.List.Base` depends on any part of `Algebra` at all. Those bundles should be defined, IMHO, in `Data.List.Bundles` (which could certainly be re-exported by `Data.List`) In this...
Also, it would probably be nice to define @dolio 's `Epic`. I would be fine with opening a fresh issue and then closing this one?
Quietly close...
Working on it. I'm first changing all of agda-categories to use the 'simpler' definition of `setoid` (as above). It requires a lot more changes than I expected (largely good). Then...
So this issue really is about findability rather than missing functionality? I have seen sum and product of setoids in the 2.0 library (but, of course, I can't find them...
Right: wherever you encounter this, probably the issue is that whoever wants a `String` should want a `Sentence` instead. Well, 80% of the time. So the details of the situation...
Operationally, your steps make sense. What's missing is that in step 3, there should some kind of "semantic analysis" pass to try to make sense of what that duplication actually...
For efficiency of checking and for having minimal dependencies, I doubt we'll ever want to use tactics in the "low level" parts of the library. So I wouldn't spend much...