Jacques Carette
Jacques Carette
So I've gone down the same rabbit hole that @sstucki did. And, unsurprisingly, rediscovered the same things. To be precise, the failure in the definition of the `counit` when using...
Progress, of sorts. The [Discrete Category](https://ncatlab.org/nlab/show/discrete+category) page on nLab is quite specific: > A category is discrete if it is both a groupoid and a preorder. That is, every morphism...
Could it be that @xplat has just solved this in PR #312 ?
Ah, I was probably reading too fast (yes, I meant that bit).
I have a (surprisingly long) list of simple category theory that's still not in the library. Planning to get back to it this summer.
I like the idea of using a record to prevent computing away valuable information. Happy with the name of the record and with `pointwise`, but less so with `funext`. I...
What's the status of this? Has a PR been done on stdlib? Should it be? This all seems like the right way to go, BTW. I might finally be in...
I think the plans are now clear. See https://github.com/agda/agda-stdlib/issues/759#issuecomment-526791198 .
My opinion on "good library development patterns": - the interface to a structure should look 'familiar'. This is why we don't use duality to define dual concepts -- otherwise the...
I waited a while on this one, as I wanted to really think about it. I definitely agree it's an issue, and that we ought to deal with it [if...