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

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

~~Definition~~

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

strict order

open interval

lower bounded open interval

Revision on June 14, 2022 at 20:15:43 by Anonymous?. See the history of this page for a list of all contributions to it.