Jacques Carette
Jacques Carette
I am definitely a big fan of having the "developer's library" be made of tons of small files with carefully crafted minimal dependencies, and a "user's library" with fewer modules...
I wonder if `map-++-commute` might have been my doing. I like that name... but I'm completely fine with `map-++` if that's the library convention.
@jamesmckinna it is indeed a philosophical disagreement. You see this PR as achieving consistency/uniformity as a complete unit, while I'd be quite happy with a sequence of PRs whose union...
`Data.List.Algebraic` seems fine. `Data.List.Traversals` could work too. Certainly should not be in `.Base`.
As it turns out, the proper notion of `Free` has recently landed in agda-categories (https://agda.github.io/agda-categories/Categories.FreeObjects.Free.html). I've been meaning to revisit free commutative monoid. I've got a [completely bit-rotted version](https://github.com/JacquesCarette/TheoriesAndDataStructures/blob/master/Structures/CommMonoid.lagda) that...
I've never used it, so I won't miss it! 😁
Looks caught in the lack of available cycles from the maintenance team. I'll assign myself, in a great fit of hope.
I don't know how to rename syntax declarations?
To be honest, I don't like either -locally or -relative. Isn't this rather a 'lifting' property? You're lifting an equality to hold at a list. In some ways, this is...
That con could be a really big one. So I headed over to `Algebra.Properties` to find out how bad it would be... and it would be fine. They are not...