The initial σ-frame in Section 11.2

[ghost]

In option 4 of the ways to construct the single type Ω in defining Dedekind cuts, it says:

On the other end of the spectrum one might ask for a minimal requirement that makes the constructions work. The condition that a mere predicate be a Dedekind cut is expressible using only conjunctions, disjunctions, and existential quantifiers over Q, which is a countable set. Thus we could take Ω to be the initial σ-frame, i.e., a lattice with countable joins in which binary meets distribute over countable joins. (The initial σ-frame cannot be the two-point lattice 2 because 2 is not closed under countable joins, unless we assume excluded middle.) This would lead to a construction of Ω as a higher inductive-inductive type, but one experiment of this kind in §11.3 is enough.

However, a lattice has a well known purely algebraic definition, with the order relation (a ≤ b) defined as (a = a ∧ b), and countable joins could be defined as a function (rational-joins:(Q → Ω) → Ω) from the function type Q → Ω to Ω, or equivalently (sequential-join:(N → Ω) → Ω) from sequences in Ω to Ω, which satisfy certain identities. As a result, it should be possible to construct Ω the initial σ-frame as a higher inductive type, rather than a higher inductive-inductive type.

[mikeshulman]

That seems plausible. @andrejbauer, do you have an opinion?