Jacques Carette
Jacques Carette
I'm now tempted to add two more records: `HasBraidedInterchange` and `HasSymmetricInterchange` with the extra fields that are in the respective modules. This would completely separate the axioms from the proofs,...
Maybe we should just move all of those one-line`Kelly` variants into the module where the original properties are proved? They would probably be more useful there? And similarly for `σ⁻¹-coherence`?...
The [ex/lex construction](https://ncatlab.org/nlab/show/regular+and+exact+completions) of exact completion would be nice to have in Agda.
We followed Agda's misnaming of universes, and named the category of (types, functions) **Sets**. This has confused people (I was replying to such a confusion just before this). I think...
See #281 for the construction. The question is then: is Setoids equivalent to its own exact completion? This is related to Michael Shulman's paper [The derivator of Setoids](https://arxiv.org/abs/2105.08152). Basically: in...
We are using `Everything.agda` as our "table of contents". As was already mentioned in #130 this is rather brutal. We should add some documentation pieces to each file, as stdlib...
Pretopos
Since it looks like Setoids is not a topos, but instead a $\Pi W$-Pretopos, I was going to implement that (i.e. Pretopos and variants). My thinking is that I should...
As was mentioned in https://github.com/agda/agda-categories/pull/191#discussion_r475220761 > in case one wants a more general preservation of limits, we can get that from the fact that strong equivalence induces adjointness, and then...
https://github.com/agda/agda/issues/4419 documents that they can be quite slow. In some places, I think variants of Yoneda is used in this way. Anything that can speed up typechecking it worth it.
In my 'negative thinking' exploration, it has become clear that I need to enrich over a monoidal groupoid too [this is how to get Setoid, since otherwise one only gets...