proposition: Proposition is_directed_below_ideal (I : rounded_ideal_completion) : is_directed rounded_ideal_completion (λ (b : ∑ b : B, b ∈ I), principal_ideal (pr1 b)).
proof: Proof. split. - exact (is_ideal_el (pr2 I)). - intros i j. assert (H := is_ideal_top (pr2 I) (pr2 i) (pr2 j)). revert H. use factor_through_squash. { apply propproperty. } intro t. induction t as ( t & p₁ & p₂ & p₃ ). refine (hinhpr ((t ,, p₁) ,, _ ,, _)) ; cbn. + intros x q. exact (trans_abstract_basis q p₂). + intros x q. exact (trans_abstract_basis q 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