Definition isTwoSided (L U : hq → hProp) : UU := ((∏ q : hq, L q <-> ∃ r : hq, L r ∧ hqlth q r) × (∏ q : hq, U q <-> ∃ r : hq, U r ∧ hqlth r q)) × ((∃ q : hq, L q) × (∃ q : hq, U q)) × (∏ q : hq, ¬ (U q ∧ L q)) × (∏ q r : hq, hqlth q r → L q ∨ U r).
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.