Proposition rounded_ideal_lub_1 (I : rounded_ideal_completion) : I ⊑ ⨆ below_ideal_directed_set I. Proof. intros x Hx. assert (H := is_ideal_rounded (pr2 I) Hx). revert H. use factor_through_squash. { apply propproperty. } intros b. induction b as [ b [ p₁ p₂ ]]. exact (hinhpr ((b ,, p₂) ,, p₁)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.CompactBasis. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions.