Homotopy Type Theory
decidable open interval > history (Rev #2)
Definition
Given a decidable strictly ordered set A A and terms a : A a:A and b : A b:A , an element c : A c:A is strictly between a a and b b if ( a < c ) = 1 (a \lt c) = 1 and ( c < b ) = 1 (c \lt b) = 1 and a decidable open interval ( a , b ) (a, b) is a dependent type defined as
( a , b ) ≔ ∑ c : A ( ( a < c ) ∧ ( c < b ) = 1 ) (a, b) \coloneqq \sum_{c:A} ((a \lt c) \wedge (c \lt b) = 1)
See also
decidable strict order
decidable closed interval?
decidable lower bounded open interval?
decidable upper bounded open interval?
Revision on June 15, 2022 at 22:47:42 by
Anonymous? .
See the history of this page for a list of all contributions to it.