Jacques Carette
Jacques Carette
Over in agda-categories we have https://github.com/agda/agda-categories/issues/342 which is about `Everything.agda` that's in the repo but doesn't typecheck. The situation is different in stdlib: `Everything.agda` is generated for the doc, but...
`Data.Bool` imports a huge amount of stuff because it does ```agda open import Data.Bool.Properties public using (T?; _≟_; _≤?_; _
In #1488 , I did not notice that `Data.Char` defines a bunch of relations which, in other parts, are done in separate sub-modules. In particular, I suggest that ```agda infix...
See [this discussion on twitter](https://twitter.com/plt_amy/status/1534242510700175360) that points to [this code on 1Lab](https://1lab.dev/Cat.Functor.Adjoint.Hom.html) that appears to do just that.
- split off the adjunction into Adjunction.Instance.BaseChange - make the code less brute force, to hopefully be more revealing as to what is going on - clean up imports
See PR #339 by @Trebor-Huang for the details. The current names are sub-optimal.
(from @sergey-goncharov ): I would suggest: 1. move the "unique" field to the bottom. It is the most sophisticated property, and must logically be the last one (this should more...
While an inside-agda solution would be better, this [HTML-level hack](https://git.amelia.how/amelia/agda-unused-imports) would be better than nothing!
@sergey-goncharov mentionned: > So, my logic was: you have canonical pullbacks in Categories.Category.Instance.Properties.Setoids.Limits.Canonical and pullbacks are only special limits, so, I though I should put binary coproducts, which are special...
There's an interesting discussion about a "proper categorical" [definition of dagger category](https://mathoverflow.net/questions/220032/are-dagger-categories-truly-evil/226426) by Peter LeFanu Lumsdaine (see the first answer). So I wonder if this should have any impact on...