proposition: Proposition rounded_ideal_lub_1 (I : rounded_ideal_completion) : I ⊑ ⨆ below_ideal_directed_set I.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.CompactBasis UniMath.OrderTheory.DCPOs.Elements.Maximal UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Examples.Propositions