Path solver

[marcinjangrzybowski]

• macro specialised for filling squares
  now it works without asusmptions about hLevel.
  I will work to avoid code duplciation with existing tactics before marking it ready for review.

[felixwellen]

I just started to look into a solver for wild categories: #1105
Maybe there is something to share? I'm not sure, just thought I point it out.

[marcinjangrzybowski]

This groupoid solver is specyficly specialised to paths (it is aware of hcomps - various ways to compose two paths).
The group solver from other PR should be easy to adapt to wild categories. equations are similar - just without laws about inverse.
I will make apropriate modifications in that PR, adn try to add solver for wild categories.

[felixwellen]

Maybe it is better to call the whole thing path solver instead of groupoid solver?

[marcinjangrzybowski]

I am experimenting but comparing result of apllying this solver for groupoid encoded as HIT vs adapting Group solver, by forcefuly typechecking proofs about groups as prooof about groupoids. Once I have both we may look at the caveats (unless they are obvious already, and someone can help me make a choice).

[marcinjangrzybowski]

for the same problem, terms for paths can be much smaller, but I am noot sure if "whiskering(?)" the proof back to groupoid wont cancel those gains anyway

[marcinjangrzybowski]

I would like to check both aproaches on some computationaly relevant example

[felixwellen]

I would expect that the approach from your group solver carried over to groupoids, is a lot more performant. But maybe my intuition is wrong. The idea is, that if you write down something like 'free groupoid on a graph' as some inductive type, then you only have what you actually need - and paths have more stuff in general.

[marcinjangrzybowski]

This is just rought intuition, but I am really curious what will happen:

In paths you can do:

 eq1 : p' ∙ ((((sym p' ∙ p) ∙ q) ∙ r) ∙ s) ≡ (((p ∙ q) ∙ r) ∙ s)  
 eq1 = 
    _
     ≡⟨ (λ i → (λ j → p' (j ∧ ( ~ i))) ∙ ((((((λ j → p' (~ j ∧ ( ~ i)))) ∙ p) ∙ q) ∙ r) ∙ s)) ⟩  
   refl ∙ ((((refl ∙ p) ∙ q) ∙ r) ∙ s)
     ≡⟨ (λ i → (lUnit ((((lUnit p (~ i)) ∙ q) ∙ r) ∙ s)) (~ i)) ⟩
   _ ∎

we do not need to apply assoc repatedly,
at first glance this is specific for paths, but I wonder, if this is not actualy representing simplier prooof for groupoid - not one based directly on groupoid laws, but one "transporting" midpoint over equivalence of "precomposing" by groupoid morhpism (lots of hand waiving here....).
proooof of this equivalence will at the end relay on those same groupoid laws, but I wonder how this will compare vs repeated applciatioon of groupoidAssoc. (especialy for even more pessymistic case, where sym p' is buried even deeper.
This is what I want to test for this solver. (at this moment it does not apply optimaisations liek this for paths, but they can be incorporated)

[marcinjangrzybowski]

Idea abowe woudl work really only for univalent groupoids, and will be ineficcient in general (I tested it)
I will restric this PR to sovler specialised only in solving paths equations (sqaures)