# 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

$\mathrm{left}\stackrel{\mathrm{segment}}{\to }\mathrm{right}\phantom{\rule{thinmathspace}{0ex}}.$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).

• circle type?

## References

Revised on December 10, 2011 00:48:04 by Mike Shulman (71.136.231.40)