Proposition is_directed_below_ideal (I : rounded_ideal_completion) : is_directed rounded_ideal_completion (λ (b : ∑ b : B, b ∈ I), principal_ideal (pr1 b)). 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.
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.