Lemma isTwoSided_OneSided : ∏ (L U : hq → hProp), isTwoSided L U → isOneSided L. Proof. intros L U H. split ; split. - exact (pr1 (pr1 (pr2 H))). - generalize (pr1 (pr2 (pr2 H))) (pr2 (pr1 (pr2 H))) ; intros H0. apply hinhfun. intros q. exists (pr1 q). intros Lq. apply (H0 (pr1 q)). split. + exact (pr2 q). + exact Lq. - intros r Lr. generalize (pr1 (pr1 H)) ; intros H0. exact (pr1 (H0 r) Lr). - intros r s Hrs. generalize (pr1 (pr2 (pr2 H))) (pr2 (pr2 (pr2 H))) ; intros H0 H1. generalize (H1 _ _ Hrs). apply hinhfun, sumofmaps. + exact ii1. + intros Us. apply ii2. intros Ls. apply (H0 s). split. * exact Us. * exact Ls. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.