types.cubical

November 23, 2015 ยท View on GitHub

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

  • pathover2
  • square2