3 ms·
I'm actually not aware of a proof in the wild equivalent to the one in Appendix B. If you know of a machine checked proof that Applicatives lift Monoids then I
by Gabriel439 12y ago
I'm actually not aware of a proof in the wild equivalent to the one in Appendix B. If you know of a machine checked proof that Applicatives lift Monoids then I would be happy to link to it.
- solomatov 12y agoI think, implementing such a proof in Agda would be a great way to learn it.
- Gabriel439 12y agoThis is an excellent suggestion. I will take a stab at this, but probably in Idris first if you don't mind. If I succeed then I will write about what I learned.
- solomatov 12y agoIf you need any help with agda, just ask.
- Gabriel439 12y agoHow do I contact you? Can I find you on the #agda channel on IRC?
- solomatov 12y agoYou can contact me via konstantin dot solomatov at google mail. I visit #agda channel from time to time.