Thomas Lamiaux

For the case of polynomial or direct sum I think there is two issues. 1. Splitting files I think it is important to have files that specify what has been...

@mortberg I would agree on the general organization you are offering. The question to me now is would be how much do you split foo

> I think it's impossible to give a general rule that applies to all structures and types, but a rule of thumb can be that each Foo should contain one...

In the folder Construction, I think we should also put things like FreeMonoid, FreeGroup that are currently in HIT Also in vo construction should the result be an AbGroup or...

Fixing the convention, I have stumbled on https://github.com/agda/cubical/blob/master/Cubical/Algebra/CommRingSolver/RawRing.agda. I was wondering if this is something that we should put in Ring ?

I was thinking about doing something like : #### Inside the Cubical Folder - Algebra - Homotopy - Cohomology - ZCohomology - Category - Codata - Core - Data I...

Maybe there should be a folder named AlgebraicGeometry ?

We also said that functions is a folder with different result about functions that felt to much to be put in Foundations. It was then moved outside. HoTT/UF have something...

@aljungstrom I miss H4 RP2 to do my proof

@mortberg Hi, just to tell you that the proof are basically done up to - @aljungstrom add a full characterization of H^n (RP²), there is only 1-3 for the moment...