## 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 ## * [[order]] * [[open interval]]