Cohomology Ring of RP2 \/ S1

[thomas-lamiaux]

Start computing the cohomology Ring of RP2 / S1

[thomas-lamiaux]

@aljungstrom is there a reason the name is conntectRP1 and not connectedRP2 ? https://github.com/agda/cubical/pull/883/files#diff-9c75fc952625dc49a8ecc86762628fb159e048def1b0ba435ca3f13180ce4aceR66

[thomas-lamiaux]

@aljungstrom @mortberg As the group are the same and the cup product is supposed to be the same, the proofs of cohomology ring is exactly the same.

As #882 , phi_1 a cup phi_1 b = 0 doesn't compute, so up to this, we'll have the computation of those rings. Axel, could you do look at this when you have sometimes ?

[thomas-lamiaux]

@mortberg Ready too.

[mortberg]

Lots of conflicts here now, please rebase on master