Proposition is_ideal_rounded {P : B → hProp} (HP : is_ideal P) {a : B} (Ha : P a) : ∃ (b : B), a ≺ b ∧ P b. Proof. assert (H := is_ideal_top HP Ha Ha). revert H. use factor_through_squash. { apply propproperty. } intros b. induction b as ( b & p₁ & 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.