[Statement of Work] category theory refactor of agda-algebras

[williamdemeo]

Description

The idea/plan is outlined in the new README_NEWS.md file.

Copilot-generated Description

This pull request updates the documentation to announce a major upcoming refactor of the Agda Universal Algebra Library, focusing on incorporating category-theoretic concepts such as polynomial functors and free monads. The changes clarify the project's direction and provide details on the planned approach, while keeping the existing API stable for downstream users.

Documentation updates and project direction:

• Updated README.md to clarify that the repository is an updated version of the Agda Universal Algebra Library, and added a pointer to the new README_NEWS.md file for ongoing developments.
• Added README_NEWS.md with a detailed announcement of the category-theory-based refactor, outlining the plan to recast operation signatures as polynomial functors, introduce algebraic theories as equations, and maintain compatibility with the current API.

Planned technical improvements:

• Described the intent to introduce a parallel layer using categorical abstractions (functors/containers, free monads, and quotient monads) for signatures, terms, and equations, with a proposed first milestone of a new module UA.Signature.Polynomial.
• Emphasized benefits such as cleaner induction principles, reusable categorical proofs, and improved documentation for both universal algebra and category theory audiences.

[JacquesCarette]

Excellent idea!