#
Homotopy Type Theory
closed interval > history (changes)

Showing changes from revision #4 to #5:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< closed interval

~~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

~~
~~
Last revised on June 14, 2022 at 20:14:54.
See the history of this page for a list of all contributions to it.