Thomas Lamiaux

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

@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 ,...

@mortberg Ready too.

could this PR be merged after all the cohomology ones ? Otherwise it going to create a lot of stuff to fix

I hadn't seen the last comment. More precisely, there is one last PR by Axel in which he is going to use polynomials, but then it should be all.

Isn't it solved ? I have this on my computer ``` From Equations Require Import Equations. Definition vec A n := { l : list A | length l =...