Paolo G. Giarrusso

https://github.com/coq-community/vscoq/issues/657 suggests problems remain and might be a duplicate.

It might also be useful to document, in [Functions.Definitions](https://agda.github.io/agda-stdlib/Function.Definitions.html), that the relations are intended to be setoid equivalences. (I don't know why this does not just pass setoids — I...

Sorry, my bad (a typo). These are the changes from the date of the Hackage release - minor ones, but I guess they would ease installation for some people: https://github.com/bitc/lushtags/compare/22294fab5ed6a215f90f36990fb0d52d0638b191...master

(Sorry to butt in, via Twitter). @RobertHarper wrote: > I don't see any advantage to applicative functors for anything, and not for type classes, unless I'm missing something. To summarize...

Dreyer's canonical example is the MkSet functor: it's a natural candidate for being an instance functor, but it's not transparent, so you need to apply it explicitly even to instances...

To be extra-clear: I don't mean to be polemic, I'm sincerely interested in @RobertHarper and @jonsterling comments/arguments on Dreyer's design (and everybody else of course, but we seem to already...

`acmart` just use existing packages, so https://tex.stackexchange.com/ might be a better place to ask such questions and get help. In this case, the documentation for `url.sty` (available at http://mirrors.ctan.org/macros/latex/contrib/url/url.pdf, or...

Oooh, seems that `Export module(coercions, canonicals, hints)` would fix this! If NES generated that when closing a namespace, `#[export] Instance` inside a namespace would work well! https://coq.inria.fr/refman/language/core/modules.html#coq:cmd.Import