Clean up Cubical

[thomas-lamiaux]

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

[thomas-lamiaux]

I was thinking about doing something like :

Inside the Cubical Folder

• Algebra
• Homotopy
• Cohomology
• ZCohomology
• Category
• Codata
• Core
• Data <= Data merge with HITs
• Foundations

Outside (indexed on a checkout)

• Papers
• Talks

???

I don't know what to (with the following folders that often contains very few files

• Benchmarks ?
• Axiom (1 file, 120L) => I don't get the principle as there is the --safe flag.
• Displayed
• Experiments => I have the felling there is a lot more outdated stuff than experiments
• Functions => I don't exactly know the content but should it be in Foundations ?
• Induction (1 file, 47L)
• Modalities (2 files, 400L)
• Reflection (3 files, 300L)
• Structures
• Syntax (1 file, 12L)

[thomas-lamiaux]

Maybe there should be a folder named AlgebraicGeometry ?

[mortberg]

Discussion to be continued :-)

[ecavallo]

Re: Axiom, the idea was that this would be the place to formulate principles like choice axioms or propositional resizing and prove relationships between them. The stdlib also has such a folder: https://github.com/agda/agda-stdlib/tree/master/src/Axiom

[thomas-lamiaux]

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 similar with a folder called MoreFoundations