There are a lot of different versions of cubical type theory and a lot of constructs are introduced: intervals, paths, faces, lines, coe, hcom, v-types, glue-types, com, fcom, ghcom, gcom, box and cap.
What is a minimal cubical type theory (counted in the amount of constructs/syntax) in order to do the same things as you can do with an intensional equality type: define/prove equalities and coercion?
