Definition coproduct_set_dcpo_lub (D : directed_set (coproduct_set_PartialOrder _ (λ x, Y x))) : lub (coproduct_set_PartialOrder _ (λ x, Y x)) D. Proof. assert (D' := directed_set_set_coproduct D). revert D'. use factor_through_squash. { apply isaprop_lub. } intros D'. induction D' as [ x D' ]. induction D' as [ D' HD ]. induction HD as [ HD H ]. use make_lub. - exact (x ,, ⨆ (make_directed_set _ _ D' HD)). - exact H. Defined.
Require Import UniMath.Foundations.All. 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.