Lemma Dcuts_of_Dcuts_bij' : ∏ E : hsubtype Dcuts, ∏ (E_bot : ∏ x : Dcuts, E x -> ∏ y : Dcuts, y <= x -> E y) (E_open : ∏ x : Dcuts, E x -> ∃ y : Dcuts, x < y × E y), Dcuts_of_Dcuts'_val (Dcuts_of_Dcuts_val E) = E. Proof. intros. apply funextfun. intros x. apply hPropUnivalence. - apply hinhuniv. simpl pr1. intros r ; generalize (pr2 (pr2 r)). apply hinhuniv. intros X. apply E_bot with (1 := pr1 (pr2 X)). apply Dcuts_lt_le_rel. apply hinhpr. exists (pr1 r). split. + exact (pr1 (pr2 r)). + exact (pr2 (pr2 X)). - intros Ex. generalize (E_open _ Ex). apply hinhuniv. intros y. generalize (pr1 (pr2 y)). apply hinhfun. intros r. exists (pr1 r). split. + exact (pr1 (pr2 r)). + apply hinhpr. exists (pr1 y). split. * apply (pr2 (pr2 y)). * apply (pr2 (pr2 r)). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.