Jacques Carette
Jacques Carette
I will note that PR #243 from stdlib 0.16 moved these around. From what I can tell, these definitions pre-date `stdlib` being on github!
I will try.
@jmougeot pushed through the work (thanks!) Yes, the naming scheme here is quite different. However, I claim that the names in this PR *make sense*. The ones for original semigroup...
In this particular case, I will definitely argue that that Fairbairn cost is worth paying, again largely because of readability. When you seem something being eliminated, it's nice to see...
> Do we want to (can we please) reexport these for rings with suitable renamings? I'd be happy to!
@Taneb I've done the renaming. I'll do the `Ring` part in a different PR, so as to not block this one.
I guess the most basic `isMonotone` should probably depend on 2 carriers and 4 relations (and a function), which is the bare minimum needed by `IsOrderHomomorphism`. I guess there is...
This is both a good direction to take, and feels like it is going to get derailed right away. Basically because Agda's features with respect to concrete Universal Algebra constructions...
Note: this part of `drasil-doclang` is also knowledge capture -- in this case of the structure of the narrative (and its commonalities and variabilities) of the SRS. So this is...
While I agree that we need to do this for 2.1, we also need to more deeply understand what's going on. The direct implementation really ought to be better! Is...