search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

Use the Monoid structure of Endomorphisms to define powering #2394

Closed JacquesCarette closed 3 months ago

JacquesCarette commented 4 months ago

As was commented by @jamesmckinna , we really ought to use the definitions from Algebra.Definitions.RawMonoid for the RawMonoid structure on Endo, both the Setoid and Propositional versions.

jamesmckinna commented 4 months ago

See this commit based off #2342 for one approach: easily incorporated on top of what you have there!