This directory contains all definitions and code that depends on the definition of the category of dimensions with faces and degeneracy operators. The definition of this category is shared throughout this directory, but abstract outside of it.
As of May 5, 2024, this category is the n-ary semicartesian cube category, with arity specified by the user on the command-line. But in the future, it will be generalized to allow multiple simultaneous "directions" of dimension, e.g. for parametricity, univalence, and display, of variable arity.
We make as many things as possible intrinsically well-typed. In particular, dimensions are represented by types satisfying a predicate, so that cubical operators are parametrized by their domains and codomains. We also implement general data structures for cubes and tubes of objects that accept faces as indices. As of May 5, 2024, this enables us to completely avoid ever "counting" the number of faces possessed by a cube, or deciding on an "ordering" of those faces other than implicitly by the order of traversal defined for cube data structures.
Here is a listing of the files in this directory, as of May 5, 2024, with brief descriptions:
- D: Repackage type-level naturals as dimensions.
- Endpoints: Dynamically control the arity of cubes.
- Arith: Arithmetic properties of dimensions like factorization and cancellation.
- Deg: Cubical degeneracies, including permutations.
- Sface: Strict faces (not including permutations).
- Face: General faces (a strict face plus a permutation).
- Op: General cubical operators.
- Bwsface: Same as strict faces, but recorded backwards.
- Tface: A strict face restricted to lie in a certain tube.
- Bwtface: Backwards version of tface.
- Insertion: A restricted permutation that preserves the relative order of part of its codomain.