1lab
1lab copied to clipboard
plt-amy
def: macros for creating copattern definitions
Description
There are a couple of places in the 1Lab where we manually eta-expand out copattern definitions by hand to get better goal display. This mostly comes up when dealing with things like subcategories/forgetful functors; Agda will very happily unfold your nicely named category into Restrict Blah, which is not particularly helpful!
Manually performing these copattern expansions is a bit of a pain, so this PR adds a small macro that performs this mechanical busywork for us. This removes the need for the declare-concrete-category macro in #375.
Checklist
Before submitting a merge request, please check the items below:
- [x] I've read the contributing guidelines.
- [x] The imports of new modules have been sorted with
support/sort-imports.hs(ornix run --experimental-features nix-command -f . sort-imports). - [x] All new code blocks have "agda" as their language.
If your change affects many files without adding substantial content, and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title with chore:.
Can this be unified with Cat.Functor.Coherence?
Should be able to! We will need to generalize make-copattern to work on functions into record types, but this shouldn't be too hard.
Should be good to go. Played around with a version of "deep" cohere! that would let us solve things like https://1lab.dev/Cat.Functor.Adjoint.html#25843 but this proved to be a bit tricky
Looks good, are there places we can use it? (Sheaves, I guess? But I'm not done writing that yet :/)
Sorry, have been quite busy recently! Sheaves would be a good place, likewise for categories of free F-algebras