Ali Caglayan

Is it VsCoq or VSCoq? Is it VS Code, VSCode or VsCode?

Can you rebase and fix the CI?

I'll create an issue in the Dune repo so we can discuss the implementation some more.

@JasonGross This has been done now right?

@JasonGross It would be nice if we can have a job for PRs that compare their build against master. What would need to be done?

I was working on this and found an anomaly https://github.com/coq/coq/issues/15042. Fixing this will have to wait till I can work out how to deal with it.

So the agda-formalisation has [a whole folder for this lemma](https://github.com/HoTT/HoTT-Agda/tree/master/theorems/homotopy/3x3). Floris seems to have written it down in the spectral library, but nothing has been attempted there. The lean and...

So I have spoken with Brunerie and he says the best way to go about it is to use cubical stuff. I have gone ahead and merged Mike's cubical branch...

So quick update. I have managed to finish the to and from functions for the equivalence. The big help was packaging things up in cubical abstraction. In order to give...

What's the alternative to rewriting? I have never really understood how coq rewrites subterms. I understand that it is using paths_ind but I don't understand how it can do that...