Lemma isOneSided_TwoSided : ∏ (S : hq → hProp), isOneSided S → isTwoSided S (λ s : hq, ∃ r : hq, hqlth r s × ¬ S r). Proof. intros S H. split ; split ; [ | | split | split]. - intros q ; split. + exact (pr1 (pr2 H) q). + apply hinhuniv ; intros r. generalize (pr2 (pr2 H) _ _ (pr2 (pr2 r))). apply hinhuniv, sumofmaps. * intros Sq ; apply Sq. * intros Sr. apply fromempty. apply Sr, (pr1 (pr2 r)). - intros q ; split. + apply hinhfun. intros r. set (s := Prelim.hqlth_between _ _ (pr1 (pr2 r))). exists (pr1 s). split. * apply hinhpr. exists (pr1 r). { split. - exact (pr1 (pr2 s)). - exact (pr2 (pr2 r)). } * exact (pr2 (pr2 s)). + apply hinhuniv. intros r. generalize (pr1 (pr2 r)). apply hinhfun. intros s. exists (pr1 s). split. * apply istranshqlth with (pr1 r). ** exact (pr1 (pr2 s)). ** exact (pr2 (pr2 r)). * exact (pr2 (pr2 s)). - exact (pr1 (pr1 H)). - generalize (pr2 (pr1 H)). apply hinhfun. intros r. exists (pr1 r+1). apply hinhpr. exists (pr1 r). split. + exact (hqlthnsn _). + exact (pr2 r). - intros q Hq. generalize (pr1 Hq). apply (hinhuniv (P := make_hProp _ isapropempty)). intros r. generalize (pr2 (pr2 H) _ _ (pr1 (pr2 r))). apply hinhuniv, sumofmaps. + exact (pr2 (pr2 r)). + intros Sq ; apply Sq. exact (pr2 Hq). - intros q r Hqr. set (s := Prelim.hqlth_between _ _ Hqr). generalize (pr2 (pr2 H) _ _ (pr1 (pr2 s))). apply hinhfun, sumofmaps. + exact ii1. + intros Sr. apply ii2, hinhpr. exists (pr1 s). split. * exact (pr2 (pr2 s)). * exact Sr. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.