Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Normal form of FreeGroup #1099

Merged
merged 16 commits into from
Apr 12, 2024

Conversation

marcinjangrzybowski
Copy link
Contributor

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

@felixwellen
Copy link
Collaborator

Are you aware of the parallel PR:
#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
Copy link
Contributor Author

marcinjangrzybowski commented Feb 7, 2024 via email

@marcinjangrzybowski
Copy link
Contributor Author

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

@marcinjangrzybowski marcinjangrzybowski changed the title Normal form of FreeGroup and GroupSolver tactic Normal form of FreeGroup Mar 24, 2024
@marcinjangrzybowski marcinjangrzybowski marked this pull request as ready for review March 24, 2024 16:35
@felixwellen
Copy link
Collaborator

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

@felixwellen
Copy link
Collaborator

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

Copy link
Collaborator

@felixwellen felixwellen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a couple of requests for comment...

Cubical/Algebra/Group/Free.agda Show resolved Hide resolved
Cubical/Algebra/Group/Free.agda Show resolved Hide resolved
Cubical/Algebra/Group/Free.agda Outdated Show resolved Hide resolved
Cubical/Foundations/Function.agda Show resolved Hide resolved
@felixwellen
Copy link
Collaborator

Is it ready to merge?

@marcinjangrzybowski
Copy link
Contributor Author

yes, thanks!

@felixwellen felixwellen merged commit f9c7655 into agda:master Apr 12, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants