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