nLab
interval type

Idea

The interval type is an axiomatization of the cellular interval object in the context of homotopy type theory.

Definition

As a higher inductive type, the interval is given by

Inductive Interval : Type
  | left : Interval
  | right : Interval
  | segment : Id Interval left right

This says that the type is inductive constructed from two terms in the interval, whose interpretation is as the endpoints of the interval, together with a term in the identity type of paths between these two terms, which interprets as the 1-cell of the interval

$$left \stackrel{segment}{\to} right \,.$$

Properties

• An interval type is provably contractible. Conversely, any contractible type satisfies the rules of an interval type up to propositional equality.

• On the other hand, postulating an interval type with definitional computation rules for left and right implies function extensionality. (Shulman).

• An interval type is a suspension type of the unit type, and the suspension of an interval type is a 2-globe type.

• An interval type is a cone type of the unit type.

• An interval type is a cubical type? $\Box^1$.

Related concepts

• interval, interval object

• suspension type

• cone type

• cubical type theory

References

• Mike Shulman, An interval type implies functional extensionality (blog post)