Comment by creata

> Keep in mind that cubical type theories are somewhat complex (in sheer amount of code),

And in computational efficiency, no? I think making an efficient implementation of a cubical type theory is still an ongoing effort.