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 = bis understood asa <= b && b >= a.
âš The API is experimental and unstable. We will break things!