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

Update `Function.Endomorphism.*` to avoid use of deprecated `Function.Equality`

Open jamesmckinna opened this issue 1 year ago • 1 comments

The #759 deprecation effort left some residues which still import (at least) Function.Equality (with a pragma to suppress the warning), notably:

  • [x] Function.Endomorphism.Setoid
  • [x] Function.Endomorphism.Propositional

which define the monoid etc. of endomorphisms (needed for a development of Foldable cf. generalising #1281 , and also now #2350 ).

UPDATED: ~~blocked on not-yet-merged #2240~~ each of the above also uses the long-since-deprecated (v1.5!) Algebra.Morphism.Is*Morphism definitions instead of updating to the ones in Algebra.Morphism.Structures ...

Should update to remove dependency on the deprecated module(s).

jamesmckinna avatar Feb 23 '24 10:02 jamesmckinna

Unfortunately the PR itself is regarded as a breaking change (even though not doing this for v2.0 was an oversight), so this issue should also get that label.

JacquesCarette avatar Apr 24 '24 01:04 JacquesCarette

So the non-breaking suggestion on #2342 would be (instead) to introduce Function.Endo.* as new modules, and deprecate the Function.Endomorphism.* modules...?

jamesmckinna avatar May 15 '24 11:05 jamesmckinna

Yes, I think that that name makes more sense than .New. I'll implement that.

JacquesCarette avatar May 16 '24 01:05 JacquesCarette