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

Showing changes from revision #0 to #1: 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

Revision on April 21, 2022 at 21:42:49 by Anonymous?. See the history of this page for a list of all contributions to it.