Normal form of FreeGroup

[marcinjangrzybowski]

Everythings work at the moment, I will request review once I will add some comments.

[felixwellen]

Are you aware of the parallel PR: https://github.com/agda/cubical/pull/1093 where I try to improve the reflection code of the ringSolver a bit. Maybe there is a chance to share some code? Something completely different: Do you know if it is substantially harder to write a groupoid-solver instead of a group solver?

[marcinjangrzybowski]

I have groupoid solver in works, it is intended as just slight extension of group solver.

On Wed, Feb 7, 2024, 10:48 AM Felix Cherubini @.***> wrote:

Are you aware of the parallel PR:

1093 https://github.com/agda/cubical/pull/1093

where I try to improve the reflection code of the ringSolver a bit. Maybe there is a chance to share some code? Something completely different: Do you know if it is substantially harder to write a groupoid-solver instead of a group solver?

— Reply to this email directly, view it on GitHub https://github.com/agda/cubical/pull/1099#issuecomment-1931665835, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACQZARWILQAC534N7YZO5DLYSNEX3AVCNFSM6AAAAABC3ZQM5WVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSMZRGY3DKOBTGU . You are receiving this because you authored the thread.Message ID: @.***>

[marcinjangrzybowski]

I removed solvers part, so that PR is only about abstract results

• uniqness of normal form for arbitrary generators

  • normalisation for dsicrete ones,
  • Bouqet is Groupoid without truncation for decidable generators

  I am opening seperate PR for WIldCatSolver wich can be specialised both for Groups and Groupoids

[felixwellen]

I am still working towards a wild cat solver, starting with free wild cats here: #1117 Should we coordinate?

[felixwellen]

I made an issue which we can use to coordinate: #1118

[felixwellen]

Is it ready to merge?

[marcinjangrzybowski]

yes, thanks!