Mayer-Vietoris

[aljungstrom]

This PR contains the Mayer-Vietoris sequence for cohomology with arbitrary coefficients. Basically directly copied from the ZCohomology version.

[felixwellen]

Do you know that Cubical.Cohomology.EilenbergMacLane.MayerVietoris stops to type-check (with unsolved metas) when you remove --experimental-lossy-unification?

[aljungstrom]

Ugh, yeah, I hadn't tried it for this version, but for the ZCohomology version I had the same problem. Didn't remember the unsolved metas, but I think type-checking is too slow even when you spell them out. My guess is that Agda is unfolding the definition of the cohomology group structure every time you try to define a homomorphism of cohomology groups.

[felixwellen]

I see. I don't know if anything bad can come from this.
Do you play around with "abstract" in situations like these?
For me, sometimes lossy-unification does it and sometimes abstract. In situations where both work, I prefer abstract, since that seems more controllable to me and it will have better support in the future (e.g. unfolding if you want to).
In case this is unclear: I'm not complaining and I have no idea if lossy-unifying things to something not really unique is bad.

[felixwellen]

We could just merge that, if you change "--experimental-lossy-unification" to "--lossy-unification" - it still checks on current master.

[mortberg]

We could just merge that, if you change "--experimental-lossy-unification" to "--lossy-unification" - it still checks on current master.

Is this the only change needed to merge the PR?

[felixwellen]

Last time I checked it was

[mortberg]

Last time I checked it was

I fixed it. Looks like many files in the library still have experimental in them though...

[felixwellen]

Last time I checked it was

I fixed it. Looks like many files in the library still have experimental in them though...

No. Did you look at the version this PR is based on?

[mortberg]

Last time I checked it was

I fixed it. Looks like many files in the library still have experimental in them though...

No. Did you look at the version this PR is based on?

Oh yeah, so it will be fine once we merge?

[felixwellen]

Yes

[mortberg]

Yes

Great! I guess I've been too busy with other things for so long that I've forgotten how git works hehe

[mortberg]

With my fix let's merge this once the CI is happy

[felixwellen]

It shouldn't be, because the CI will use an old version of agda ;-)

[felixwellen]

If we want the CI to be happy, we will need to rebase onto master/merge master.

[felixwellen]

Ok, I guess that means I have a wrong idea about what the CI actually does.

[mortberg]

Ok, I guess that means I have a wrong idea about what the CI actually does.

Lol, you made me very confused just now...

[mortberg]

@felixwellen do you want to merge?

[felixwellen]

I don't get why it didn't fail, but let's just merge it - I have time to fix things, if it fails.

[mortberg]

I don't get why it didn't fail, but let's just merge it - I have time to fix things, if it fails.

I guess the changes are compatible with the state of master and the CI has confirmed that it doesn't fail after merging?