agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

Deprecate or refactor `Algebra.Construct.Subst.Equality`

Open MatthewDaggitt opened this issue 4 years ago • 5 comments

This can now be implemented entirely via Algebra.Morphism

MatthewDaggitt avatar Mar 04 '21 04:03 MatthewDaggitt

So it seems as though Algebra.Morphism ended up deprecated, and Subst.Equality lived to fight another day... so close this now?

jamesmckinna avatar May 11 '24 12:05 jamesmckinna

I should have been more precise. It can be implemented by the classes below Algebra.Morphism...

MatthewDaggitt avatar Jul 11 '24 02:07 MatthewDaggitt

Ah! ... thanks for the signpost... and for revisiting a dormant issue... worth knocking off for v2.2?

jamesmckinna avatar Jul 11 '24 10:07 jamesmckinna

As always, if someone is willing to do it :smile:

MatthewDaggitt avatar Aug 14 '24 08:08 MatthewDaggitt

I'll give it a try.

JacquesCarette avatar Aug 14 '24 20:08 JacquesCarette