Homotopy Type Theory closed interval > history (Rev #4)

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)