Thomas Lamiaux

@mortberg done

done

We talked about it, the idea would be to - Put those lemma in named module so that people have to open it to acces it. - Add comment on...

Yes indeed no link. I find the unit. Nat export Nat.literals that in turn export a some things publicly. Is that normal : - Base is not self contained -...

As it can be seen in #824 for instance https://github.com/agda/cubical/pull/824/files#diff-4a2a2c1432b474e7043879a7522d65805ad61112d16267e130091b89d4ee29b1L7, there is still a lot of useless import that can be removed.

@aljungstrom @mortberg On this proof, the function gets more complicated, as there is 2 variables, there is [3 trivial cases](https://github.com/agda/cubical/pull/879/files#diff-55f172e9e9b317a17b9e9b3d90476fcea449b07dbd2e9ea824266ee27485ac27R220) This annoying because, the [proof of the cup-product](https://github.com/agda/cubical/pull/879/files#diff-55f172e9e9b317a17b9e9b3d90476fcea449b07dbd2e9ea824266ee27485ac27R253) become hard...

Hi @mortberg and @aljungstrom, I have spend two days computing `S2 \/ S4` because it is a simpler example. So the ring is `Z[X,Y]/.` Though I have a very weird...

I don't have the time right now but if someone wants to do it, I have the following idea : There are actually four potential definitions of the polynomials in...

update : #798 is going to add full CommRing structure around 4 that was missing and prove the equivalence. Hence in the library, there is going to be 4 1...

I was thinking that it is important to have specific files rather than modules (also in more general case). This way it is easier to find something in the library...