This PR reorganizes the cube fillers in library. They've been renamed uniformly, deduced as corollaries of the extend operation and now collected in Cubical.Foundations.HLevels.Fillers. There are still some left in Cubical.Foundations.Prelude due to their preliminary nature. @mortberg
To achieve this, I have to separate the basic definitions and facts about h-levels from Cubical.Foundations.HLevels into a new file Cubical.Foundations.HLevels.Base. Additionally, I separated the cube types in Cubical.Foundations.Prelude to the file Cubical.Foundations.Cubes.
This PR reorganizes the cube fillers in library. They've been renamed uniformly, deduced as corollaries of the
extendoperation and now collected inCubical.Foundations.HLevels.Fillers. There are still some left inCubical.Foundations.Preludedue to their preliminary nature. @mortbergTo achieve this, I have to separate the basic definitions and facts about h-levels from
Cubical.Foundations.HLevelsinto a new fileCubical.Foundations.HLevels.Base. Additionally, I separated the cube types inCubical.Foundations.Preludeto the fileCubical.Foundations.Cubes.