Yes, that is the gist of it: we can't do this. Negative results need to be communicated, too! But that's not all there is to it. The fact we do present a type almost identical to Path and Interval with self-types, and the fact that such type has almost identical proofs of relevant theorems (like `funext`), yet no proof of the very important `transp`, does make a strong hint that further additions to the core are necessary. It also gives us a direction, and even some hints of how the implementation could be simplified. Keep in mind that cubical type theories are somewhat complex (in sheer amount of code), but there is no evidence they can't be simplified further. Kind has a goal to keep its core as simple as possible. Being able to express all the Coq inductive proofs in a 700-LOC core is a miracle, isn't it?
> I suspect you will never be able to!
That makes no sense! In the worst case we could just go ahead and implement CubicalTT on Kind's Core. We just don't want to commit to that until we're sure there isn't a way to simplify it, even if slightly.
> I suspect you will never be able to!
That makes no sense! In the worst case we could just go ahead and implement CubicalTT on Kind's Core. We just don't want to commit to that until we're sure there isn't a way to simplify it, even if slightly.