#
Homotopy Type Theory
upper bounded open interval > history (changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

## Definition

< open interval

~~Given a ~~

~~strictly ordered type~~~~ ~~~~$A$~~~~ and a term ~~~~$a:A$~~~~, an ~~**upper bounded open interval**~~ ~~~~$(a, \infty)$~~~~ is a dependent type defined as~~~~
~~$(-\infty, a) \coloneqq \sum_{b:A} (b \lt a)$

~~
~~## See also

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