# Homotopy Type Theory closed interval > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

## Definition

Given an

ordered type $A$ and terms $a:A$ and $b:A$ a closed interval $[a, b]$ is a dependent type defined as

$[a, b] \coloneqq \sum_{c:A} (a \leq c) \times (c \leq b)$