Why is the interval not a type but a pretype?

Question

In Section 3.3 of Naive cubical type theory (Bruno Bentzen):

We suggested above that every type is Kan. In fact, the interval is the only exception to this rule, since we have been implicitly treating it as a “type”, but it actually does not support any Kan operations. Indeed, if the interval were Kan, then the identity path $$ \lambda i.i : \mathrm{path}_{\mathbb{I}}(0, 1) $$ would have an inverse, but what could that be? To deal with this fact, we adopt the convention that the interval can only occur as the antecedent of a function type (hence, the interval may be called a “pretype”).

I could not understand the fact that the path $\lambda i.i$ does not have an inverse. Isn't it simply $(\lambda i.i)^{-1}:\mathrm{path}_{\mathbb I}(1,0)$?

Answer 1

I think the answer to this question is probably a lot more complicated than that particular paper wants to get into. It's trying to present a simplified, less formal version of cubical type theory, while the reason behind this aspect has to do with technical details.

In a lot of formal presentations of cubical type theory, the interval isn't a type at all. Instead, there are actually two sorts of variables in the theory. One sort ranges over types, like in ordinary type theory. The other ranges over the interval, and is related to the fact that that every type is a presheaf on the cube category. (Pre)sheaves are related to variable contexts so this is potentially a general technique.

So, if you arrange the 'naive' (or even formal) theory to have a sort of 'pre-type' for interval variables, it generally does not make sense to treat it like a normal type, because it just has a different status. The operations on such a pre-type are supposed to correspond to things that can happen in the cube category, and the genuine types (which are presheaves) aren't even in that category. The cube category generally lacks other structure, too. It might not be closed, just Cartesian. It might not even be Cartesian. etc.

Now, the Yoneda embedding gives you an object representing the cube category interval in the cubical set category, so you might imagine that you could make that your 'type', since it would behave more like one. However, then it is still just a fact that this cubical set is not Kan (I think that's a relevant citation; I don't have the expertise to explain why this is). So it is still not a type but a 'pre-type', since the Kan operations don't necessarily work on it, like in the paper you're reading. I think this is a more general phenomenon, where the whole cubical set category contains many things that only qualify as 'pre-types' not types, because only ones with additional structure qualify as the latter. I imagine this could be formally presented as a "two level type theory," or something similar.

You can get a weakly equivalent object by "fibrant replacement." So you could consider it to be the interval that is an actual type. I think an example of that would be a higher-inductive definition of 'the interval' like:

data Intv : Type where
  zero one : Intv
  seg : zero = one

I'm not sure if anything in the paper you're reading would go awry with imagining $\mathbb{I}$ to actually be such a type. In a formal theory, (I think) the purpose of the pre-types would be to distinguish more fine-grained detail than the types are allowed to. E.G. two pre-types might be considered distinct even though they have equivalent fibrant replacements. The above inductive type is equivalent to the unit type, but obviously something about it is supposed to not be the same as the unit type. I think that something is that it is presented by a different pre-type.