Definition coproduct_dcpo_lub (D : directed_set (coproduct_PartialOrder X Y)) : lub (coproduct_PartialOrder X Y) D. Proof. assert (D' := directed_set_coproduct D). revert D'. use factor_through_squash. { apply isaprop_lub. } intros D'. induction D' as [ D' | D' ]. - induction D' as [ D' H ]. use make_lub. + exact (inl (⨆ D')). + exact H. - induction D' as [ D' H ]. use make_lub. + exact (inr (⨆ D')). + 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.