Category of groups, uniqness of adjunctions

[marcinjangrzybowski]

• Grp is Univalent Category
• opposite adjunctions
• freeGroupFunctor adjoint to forgeting group structure
• lemmas about ^opF and natural transformations
• hsome module parameters promoted to generalised variables

PR contains some strict isomorphisms, but I was unable to apply declStrictIsoToEquiv macro to them (agda stalled)

[marcinjangrzybowski]

I developed this in agda 2.6.4, and see now that 2.6.3 in CI is not able to infere all metas. Is there plan to migrate cubical to 2.6.4 in near future? if not I will just make it more explicit.

[felixwellen]

There is a plan - I think I'll get to that in the next days.

[felixwellen]

If you want to use cat-solvers with agda 2.6.4, you can use the change in this PR #1050

[marcinjangrzybowski]

I made definitions slightly more explicit to make it work with 2.6.3

[marcinjangrzybowski]

it seams that 2.6.3 is not able to fully make use of the fact that ^opF is strict incolution

[felixwellen]

Please rebase/merge master to fix the CI issue

[felixwellen]

... to have these things. I guess you are working on things which will use this stuff in conjunction...

[marcinjangrzybowski]

Yes :) expect next PR this weekend!