Module Cubical.Dim

The abstract syntax of the Cartesian interval.

type dim =
| Dim0

The left endpoint of the abstract interval.

| Dim1

The right endpoint of the abstract interval.

| DimVar of int

In cooltt, most dimension variables are represented as natural numbers (pointers into the context).

| DimSym of Basis.Symbol.t

Some dimension variables must be generated in a globally fresh way (e.g. when computing under a binder).