Homotopy Type Theory lower bounded open interval > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

< open interval

Given a

strictly ordered type AA and a term a:Aa:A, a lower bounded open interval (a,)(a, \infty) is a dependent type defined as

(a,) b:A(a<b)(a, \infty) \coloneqq \sum_{b:A} (a \lt b)

See also

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