Definition isOneSided (S : hq → hProp) : UU := ((∃ r : hq, S r) ∧ (∃ r : hq, ¬ S r)) × (∏ r : hq, S r → ∃ q : hq, S q ∧ hqlth r q) × (∏ r s : hq, hqlth r s → S r ∨ ¬ S s).
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.