Post #2142731

The problem with implementing cubical is that we have so many variables of the same type, so really nothing saves us from making scope errors, not even dependent types and intrinsic scopes