0
$\begingroup$

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?

$\endgroup$

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.