Lex van der Stoep
Lex van der Stoep
Dependent types ;)
Hey Matthew, I started working on this issue, and struggled to get my head around the following: if `P` is a relation on elements of type `A`, and `Q` is...
Could a bi-implication version of [`P =[ f ]⇒ Q`](https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Indexed/Heterogeneous/Core.agda) work as well? The type of the lemmas would then be along the lines of: `map⁺ : ∀ {f xs}...
It uses [ARK.io](https://ark.io) in the backend. You can start by having a look there if you want to find out more about it. Good luck!
Thanks for reviewing this so quickly! I was about to mark the PR as a draft to fix the usage of `IsNonAssociativeRing`, but you beat me to it. About the...
Sounds like a plan!
@jamesmckinna Updated the PR to be 'ready to go'. I'll tackle the almighty `CHANGELOG` merge conflict when the time comes...