WildCat, Groupoid, Group - Solvers

[marcinjangrzybowski]

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]

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]

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

[marcinjangrzybowski]

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.

[felixwellen]

Might be better to use ´´´module C' = ...´´´ instead of the * which can be confused with the \ast

[marcinjangrzybowski]

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.

[marcinjangrzybowski]

this works, but will have some overlap (~400 LOC) with #1150 , so I will until 1150 is resolved