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

## See also

Revision on May 12, 2022 at 00:45:17 by
Anonymous?.
See the history of this page for a list of all contributions to it.