Thomas Lamiaux

Cohomology Ring of S2 \/ S4

2

PR to compute the cohomology ring of S2 \/ S4 which should be Z[X,Y]/ For CP2 / S2 \/ S4, this should give an example where the groups are the...

Cohomology Ring of RP2 \/ S1

2

Start computing the cohomology Ring of RP2 \/ S1

Cohomology Ring of the Klein Bottle

3

Starting computing the cohomology ring of K²

RP2

3

Add RP2, in progress

CP2

1

@aljungstrom @mortberg this now the one about CP2 The missing lemma https://github.com/agda/cubical/pull/846/files#diff-698ce42781a40deec28df98fa92612bbea8a1672b47c9cda870dd00d22ef2e8dR441

Refactor Int ?

1

Currently in Int there is a bunch of properties like +Comm that maybe should be hidden. Indeed they are often in double with opening a RingStr

Agda Nat exports Unit somehow

5

I was working on a file and I couldn't get how I was using Unit without importing it. Turned out it was exported by imported Nat. I couldn't figure out...

Clean up Cubical

5

This an issue to discuss the general organization of the Cubical library first layer of folders.

Splitting files in Algebra

13

We were talking about the files organization inside of Algebra. The question being when should we split files ? For instance, there is the [Group folder ](https://github.com/agda/cubical/tree/master/Cubical/Algebra/Group) where everything are...

Useless import and make

2

When cleaning the code, I have realized that there is actually a lot of files that import module that are not used at all. This annoying because when renaming or...