Jacques Carette
Jacques Carette
Suggestion: create a local alias `L` for `List` for the scope of those proofs?
Local vs global...
Very nice. A lot of proofs in agda-categories could be made more digestible for humans with such machinery, as quite a lot of work is spent on dealing with cong...
What am I missing? I'm seeing the word 'instance' all over the comments (and in the review) but none in the code?
> My bad, or at least, my possible misuse of the term-of-art when I should say something else, like 'dictionary'. In my mind, but not, I think (!?), unique to...
I think @jamesmckinna is simply asking: can you explain in plain English what you are trying to achieve here? It's not clear just from the code itself.
Strongly agree with > Proposal: we add actual bundled homomorphisms for all the algebraic `Structures` in the library, as I ended up having to define some of these myself in...
Since most of stdlib is now `Setoid` based, I think it would make sense to continue that way, and then specialize to propeq for convenience when strictness is wanted. Let...
I was hoping to start migrating the basic parts of `agda-categories` to `agda-stdlib`, so that `Category`, `Functor` and friends could be 'right'. I think that things in `agda-categories` have settled,...
Right, this serves as a nice reminder for me to start a design discussion on just that.