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

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


< open interval

Given a

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

(,a) b:A(b<a)(-\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.