This library implements cofibrations in Cartesian cubical type theory as described in the paper Syntax and models of Cartesian cubical type theory, with the following two extensions:
- Cofibration variables.
- Inequalities between dimension variables. The equation
a = b
is understood asa <= b && b >= a
.
âš The API is experimental and unstable. We will break things!