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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.