agda-stdlib
agda-stdlib copied to clipboard
Deprecate or refactor `Algebra.Construct.Subst.Equality`
This can now be implemented entirely via Algebra.Morphism
So it seems as though Algebra.Morphism ended up deprecated, and Subst.Equality lived to fight another day... so close this now?
I should have been more precise. It can be implemented by the classes below Algebra.Morphism...
Ah! ... thanks for the signpost... and for revisiting a dormant issue... worth knocking off for v2.2?
As always, if someone is willing to do it :smile:
I'll give it a try.