Cubical Types:
The files path and pathover are in the init/ folder.
- square: square in a type
- cube: cube in a type
- squareover: square over a square
- cubeover: cube over a cube
The following files are higher coherence laws between operators defined in the basic files