In cubical type theory, why are there function types that accept intervals as arguments when there are already a path type?

Question

In the original CCHM paper, a path can be constructed using an interval and two endpoints. However, why do I see in some other papers some types like I -> A in which I is the interval type and A is a normal type? It seems that values of I -> A are constructed by a normal lambda. Why are these function types needed while there is another binding construct for path types? (e.g. <i> a i) If types like I -> A is really needed, why is it not present in CCHM?

Answer 1

The "normal" function type former expects fibrant domain and codomain types. Fibrant means that the type supports Kan operations. I does not support Kan operations, so I -> A can't be a normal function type. I -> A can be instead viewed as a path type where the endpoints are not constrained in the type. It's called "line type" in the yacctt and cctt implementations.

Whenever we don't want to specify the endpoints of a path, the line type is more convenient than the path type, and it also possibly improves type checking speed because there's less data to track.

For an example, here's a cctt proof that coercion is an equivalence. Th f', g', linv' and rinv' helper definitions all have dependent line types; they take one or more I arguments and that's translated to line types during type checking. Here, the endpoints of the definitions can be already computed on demand just by instantiating the I arguments to 0 or 1, so there's no need to specify them in the types. You can see that the return types of helper definitions are pretty simple, just A i or A r. Without line types, we'd have needed to specify all endpoints there, which are pretty big expressions, and it gets more annoying if we have multiple I arguments, because then we have to give 2^N endpoints in an iterated path type.

A generalization of both path types and line types is called extension type. This is supported in cooltt. It lets us abstract over an arbitrary number of I arguments at once, plus we can put a boundary condition on the result. In once special case, we have one interval argument and the 0 and 1 endpoint specification, so we get path types. If we omit the endpoint specification, we get line types. It's also possible to e.g. specify just one endpoint, and in general we may have N-dimensional cubes with some faces being specified in the type.