Jacques Carette
Jacques Carette
Would there be something to learn from @gelisam 's [premonoidal](https://github.com/gelisam/premonoidal) solver?
So is this completely stalled then?
I agree that the order in `Product` is the better one. Especially as one sees uses of converse to prove very simple things using pullback, which is a hint that...
Sorry for the slow answer. I quite like the sample documentation for Category.Core. @HuStmpHrrr we could consider moving some of the files to literate Agda. Also, there is a restructured...
1. Any code where we'd like to have more extensive documentation that displays well (with extra links, nice formatting, etc in the comments) 2. I think that's still evolving. I...
I actually ran a full load of this library with those options turned on. I have the results saved somewhere, I'll upload 'soon'.
Indeed. Sometimes it's useful to be able to say you have 2 monoidal structures on the same category (which is what option 1 makes easiest), but sometimes you have a...
So option 2 is basically along the lines of "a category C along with extra structure that makes it into a Monoidal Groupoid" while option 3 is "a Monoidal Groupoid"....
Thanks for pointing out this development. Porting this would be nice, but a non-trivial amount of work. Especially as `Ofes` themselves really belong in stdlib, and then the categorical work...
Same comment as on #40: soon. And this is very interesting!