Lemma weqOneSidedDcuts : weq (∑ S : hq → hProp, isOneSided S × ∏ q : hq, q < 0 → S q) Dcuts. Proof. set (f := (λ (D : ∑ S : hq → hProp, isOneSided S × (∏ q : hq, q < 0 → S q)), make_Dcuts (λ r : NonnegativeRationals, pr1 D (pr1 r)) (isOneSided_Dcuts_bot (pr1 D) (pr1 (pr2 D))) (isOneSided_Dcuts_open (pr1 D) (pr1 (pr2 D))) (isOneSided_Dcuts_corr (pr1 D) (pr1 (pr2 D)))) : (∑ S : hq → hProp, isOneSided S × (∏ q : hq, q < 0 → S q)) → Dcuts). assert (Hg : ∏ (D : Dcuts) (q : hq), q < 0 → sumofmaps (λ _ : 0 > q, htrue) (λ Hq : 0 <= q, pr1 D (q,, Hq)) (hqgthorleh 0 q)). { intros D q Hq. induction (hqgthorleh 0 q) as [Hq' | Hq']. { exact tt. } apply fromempty. refine (hqlehtoneghqgth _ _ _ _). - apply Hq'. - unfold hqlth in Hq. exact Hq. } set (g := (λ D : Dcuts, (λ q : hq, sumofmaps (λ _ : 0 > q, htrue) (λ Hq : 0 <= q, pr1 D (q,, Hq)) (hqgthorleh 0 q)),, isDcuts_OneSided (pr1 D) (is_Dcuts_bot D) (is_Dcuts_open D) (is_Dcuts_corr D),, Hg D) : Dcuts → ∑ S : hq → hProp, isOneSided S × (∏ q : hq, q < 0 → S q)). apply (weq_iso f g). - intros D. simple refine (subtypePath_prop (B := λ _, make_hProp _ _) _). + apply isapropdirprod. * 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. * apply impred_isaprop ; intro q. apply isapropimpl, propproperty. + apply funextfun ; intros q. apply hPropUnivalence. * change (sumofmaps (λ _ : 0 > q, htrue) (λ _ : ¬ (0 > q), pr1 D q) (hqgthorleh 0 q) → pr1 D q). induction (hqgthorleh 0 q) as [Hq | Hq]. ** intros _. apply (pr2 (pr2 D)). exact Hq. ** intros H ; apply H. * change (pr1 D q → sumofmaps (λ _ : 0 > q, htrue) (λ _ : ¬ (0 > q), pr1 D q) (hqgthorleh 0 q)). intros Dq. induction (hqgthorleh 0 q) as [Hq | Hq]. ** exact tt. ** exact Dq. - intros D. apply subtypePath_prop. apply funextfun ; intros q. apply hPropUnivalence. + change (sumofmaps (λ _ : 0 > pr1 q, htrue) (λ Hq : ¬ (0 > pr1 q), pr1 D (pr1 q,, Hq)) (hqgthorleh 0 (pr1 q)) → pr1 D q). induction (hqgthorleh 0 (pr1 q)) as [Hq | Hq]. * apply fromempty. refine (hqlehtoneghqgth _ _ _ _). ** exact (pr2 q). ** exact Hq. * intros H. assert (Hq1 : q = (pr1 q,, Hq)) by (apply subtypePath_prop ; reflexivity). rewrite Hq1 ; exact H. + change (pr1 D q → sumofmaps (λ _ : 0 > pr1 q, htrue) (λ Hq : ¬ (0 > pr1 q), pr1 D (pr1 q,, Hq)) (hqgthorleh 0 (pr1 q))). intros Dq. induction (hqgthorleh 0 (pr1 q)) as [Hq | Hq]. * apply fromempty. refine (hqlehtoneghqgth _ _ _ _). ** exact (pr2 q). ** exact Hq. * assert (Hq1 : q = (pr1 q,, Hq)) by (apply subtypePath_prop ; reflexivity). rewrite Hq1 in Dq ; exact Dq. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.