Definition coproduct_dcpo_inl_lub (D : directed_set X) : lub (coproduct_PartialOrder X Y) (directed_set_comp (inl_monotone_function X Y) D). Proof. use make_lub. - exact (inl (⨆ D)). - split. + abstract (intro i ; apply (less_than_dcpo_lub _ _ i (refl_dcpo _))). + abstract (intros y Hy ; cbn in y, Hy ; induction y as [ x' | y' ] ; [ exact (dcpo_lub_is_least D x' Hy) | ] ; cbn in * ; assert (w := directed_set_el D) ; revert w ; use factor_through_squash ; [ apply isapropempty | ] ; exact Hy). 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.