Interval (HIT)

Definition

The interval $I$ is a Higher Inductive Type with two distinct points and a path connecting them.

Constructors:

• $i0:I$
• $i1:I$
• $\mathrm{seg}:i0=i1$

The interval represents the unit interval $[0,1]$ from topology as a type with two endpoints and a path between them.

Properties

The interval is contractible: it is equivalent to the Unit Type. However, its elimination principle is computationally useful for defining functions out of other HITs.

Related Concepts

Higher Inductive Type Circle (HIT) Suspension (HIT) Path Type Identity Type