WildCat, Groupoid, Group - Solvers

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

441 stars 134 forks source link

WildCat, Groupoid, Group - Solvers #1119

Open marcinjangrzybowski opened 3 months ago

marcinjangrzybowski commented 3 months ago

Also handles functor laws (for arbitrary many, and arbitrary nested functors)

Examples in: WildCat Group Groupoid

everything works for now

TODO:

docs/comments,
resuse code from other solvers where possible
allow using usual funcotr for grooups, categories and groupoids (now they have to be wraped into equivalent WildFunctor type)

marcinjangrzybowski commented 3 months ago

Generic Solver (in Tactcics/WildCatSolver/Solvers.agda). Can be instantiated with WildCatInstance, and optionaly nverses if they are present (for Groupoids, and Groups). Examples of that specialisation are in Solver.agda files.

felixwellen commented 3 months ago

Very nice! How does this relate to your open PR on Groups?

marcinjangrzybowski commented 3 months ago

I made elevant comment in that PR, they are independent now, previous PR is more abstract now, I removed solver and left results about uniqness of normal form without discretness asumption.

marcinjangrzybowski commented 2 months ago

Current path solver from this PR is really specialised groupoid solver, and I thing that in cubical path sovler shoould be from the start generalised to higher dims (I am preparing PR on this). I plan to remove path solvler from this and then submit this PR with remainging solvers( WIldCat, Cat, Groupoids, Groups) for review this weekend.