Jacques Carette
Jacques Carette
`_≡?_` seems principled. We might want to leave `_≟_` around as a convenience alias for a while, i.e. longer than the usual deprecation cycle.
The basic idea is very good - the chunk hierarchy should indeed be used, instead of forcing the work onto the 'user'. I'm not so happy with the implementation scheme....
> We've now gone 180 ∘ on the chunk nesting. Yes we have!
We were too busy just creating the library to pay (enough) attention to being systematic about right/left, algebraic vs diagrammatic order, etc. (Same happened with `stdlib` and we're suffering because...
Thanks for letting me know. Would it be worth my re-reviewing this in the mean time?
Will re-review soon. It might still be blocked because the CI is currently broken! I've been wanting to fix that, but have not had the time for that either.
(closing and reopening to get CI to run)
Build failed with ``` /home/runner/work/agda-categories/agda-categories/src/Categories/Bicategory/Construction/Bimodules/TensorproductOfHomomorphisms.agda:98.5-64: warning: -W[no]OpenImportAbstract `abstract' does not have any effect on `open' so better place this statement outside of the abstract block when scope checking the declaration...
ping: could you look at the build failure please?
I would suggest also testing with 1lab, TypeTopology and agda-categories before making such conclusions.