Contents

# Contents

## 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$.