Rationalize interval terminology

[lowasser]

I think we will shortly want other kinds of intervals, so it might be time to organize terminology.

I'm not sure what the best name for rational intervals is, but

• "bounded intervals in a poset" might suffice for the order theory definition; with nonstrict inequality there's only one kind of interval bounded on both sides
• "compact interval" accurately describes the kind of interval on the reals currently described as closed

[fredrik-bakke]

Compactness has a topological meaning, which is how it should be used: it means that any open cover of a space (here interval) has a finite subcover. It's a theorem in topology that every compact subspace of the reals is a union of closed intervals. There's also a weaker cousin to compactness called "sequential compactness": a space X is sequentially compact if every sequence in X has a convergent subsequence.

[fredrik-bakke]

If you are thinking of intervals $[a , b]$ in $ℚ$ then isn't the terminology clear? This is called a closed interval in $ℚ$, or rational closed interval. I think I'm misunderstanding the question. The difference between a closed $[a,b]$ and an open interval $(a,b)$ is precisely that $x \in [a,b]$ iff $a \leq x \leq b$ while $x \in (a,b)$ iff $a < x < b$.

[fredrik-bakke]

In essence, closed intervals come from partial orderings and open intervals come from strict orderings.

[lowasser]

Compactness has a topological meaning, which is how it should be used: it means that any open cover of a space (here interval) has a finite subcover. It's a theorem in topology that every compact subspace of the reals is a union of closed intervals. There's also a weaker cousin to compactness called "sequential compactness": a space X is sequentially compact if every sequence in X has a convergent subsequence.

The only viable definition of compactness in constructive contexts -- discussed in detail in e.g. HoTT -- is a closed, totally bounded set; this is classically equivalent to all classical forms of compactness, and is already defined in unimath. PRs currently in flight prove this definition of compactness for what we're currently calling closed intervals in the reals.

The primary issue is that I want to define notions of interval on the real numbers, at least, which are not necessarily bounded even if they are topologically closed -- but a compact interval is indeed a closed and bounded interval, the notion we're currently describing. Renaming the current notion of closed interval in the real numbers to compact interval is more-correct and frees up the term "closed interval" to definitions that include [0, \infty).

Notably, this is also the terminology used by Bishop in Foundations of Constructive Analysis.

[fredrik-bakke]

Will your proposed definition of compact interval also include singletons, i.e. [a,a]?

[fredrik-bakke]

otherwise it should at least be called a proper compact interval

[fredrik-bakke]

I read the section in the HoTT book now. Their definition of Heine–Borel compactness for inductive covers seems to me to be a somewhat reasonable substitute for compactness. Note that we can define higher inductive types in agda-unimath using postulates, if you want some advice on that I'd be happy to oblige. It's not demonstrated anywhere that totally bounded cauchy complete metric spaces are Heine–Borel compact for inductive covers though, is this known?