Lemma weqTwoSidedOneSided : (∑ L U : hq → hProp, isTwoSided L U) ≃ (∑ S : hq → hProp, isOneSided S). Proof. set (f := (λ (LU : ∑ L U : hq → hProp, isTwoSided L U), pr1 LU,, isTwoSided_OneSided (pr1 LU) (pr1 (pr2 LU)) (pr2 (pr2 LU))) : (∑ L U : hq → hProp, isTwoSided L U) → ∑ S, isOneSided S). set (g := (λ S : (∑ S : hq → hProp, isOneSided S), pr1 S ,, (λ s : hq, ∃ r : hq, r < s × ¬ pr1 S r) ,, isOneSided_TwoSided (pr1 S) (pr2 S)) : (∑ S, isOneSided S) → ∑ L U : hq → hProp, isTwoSided L U). apply (weq_iso f g). - intros LU. change (pr1 (g (f LU)),, pr2 (g (f LU)) = pr1 LU,, pr2 LU). apply pair_path_in2. simple refine (subtypePath_prop (B := λ _, make_hProp _ _) _). + apply isapropdirprod. * apply isapropdirprod ; apply impred_isaprop ; intro q ; apply isapropdirprod ; apply isapropimpl, propproperty. * apply isapropdirprod. ** apply isapropdirprod ; apply propproperty. ** apply isapropdirprod. *** apply impred_isaprop ; intro q. apply isapropneg. *** apply impred_isaprop ; intro q. apply impred_isaprop ; intro r. apply isapropimpl, propproperty. + apply funextfun ; intros q. apply hPropUnivalence. * apply hinhuniv. intros r. generalize (pr2 (pr2 (pr2 (pr2 (pr2 LU)))) _ _ (pr1 (pr2 r))). apply hinhuniv, sumofmaps. { intro Lr ; apply fromempty, (pr2 (pr2 r)), Lr. } intros Uq ; apply Uq. * intros Uq. generalize (pr1 (pr2 (pr1 (pr2 (pr2 LU))) _) Uq). apply hinhfun. intros r. exists (pr1 r). split. ** apply (pr2 (pr2 r)). ** intros Lr. apply (pr1 (pr2 (pr2 (pr2 (pr2 LU)))) (pr1 r)). split. *** apply (pr1 (pr2 r)). *** apply Lr. - intros S. simple refine (subtypePath_prop (B := λ _, make_hProp _ _) _). + apply isapropdirprod. * apply propproperty. * apply isapropdirprod. ** apply impred_isaprop ; intro r. apply isapropimpl, propproperty. ** apply impred_isaprop ; intro r. apply impred_isaprop ; intro s. apply isapropimpl, propproperty. + reflexivity. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.