Interval

Abstract

The interval $\mathbb{I}$ is a primitive syntactic entity in cubical type theory providing the domain for path abstraction and application. It is not a standard fibrant types.

Definition

The interval $\mathbb{I}$ is a structural object equipped with endpoints $i_0,i_1:\mathbb{I}$ and various algebraic operations depending on the specific cubical model, such as De Morgan Involution or Cartesian structures. We use it to parameterize paths: a path in a type $A$ is a function $\mathbb{I}\to A$.

Typal Status

The premise that $\mathbb{I}$ is not a standard type is correct. However, the reasoning that this is due to contractibility is imprecise.

We cannot internally state or prove that $\mathbb{I}$ is contractible. Forming the proposition ${\Sigma }_{x:\mathbb{I}}{\Pi }_{y:\mathbb{I}}(x{=}_{\mathbb{I}}y)$ requires forming the identity type over $\mathbb{I}$, but the target of an identity type must be a standard fibrant type.

Instead, $\mathbb{I}$ is excluded from the standard universe of types because it is a pre-type that lacks the structure of a Kan complex. It does not support Kan operations such as composition and transport. If $\mathbb{I}$ were admitted as a standard type, it would violate univalence and collapse the higher-dimensional structure of the theory. In implementations like Cubical Agda, $\mathbb{I}$ belongs to a dedicated, non-fibrant universe IUniv. While we can construct $\Pi$-types over $\mathbb{I}$ to form paths, we cannot treat $\mathbb{I}$ itself as an internal space or pattern-match on its endpoints.

See also

Cubical Type Theory Homotopy Type Theory Kan Complex

References

• Cubical Type Theory: a constructive interpretation of the univalence axiom