Definition coproduct_dcpo_incl_lub (x : X) (D : directed_set (Y x)) : lub (coproduct_set_PartialOrder _ (λ x, Y x)) (directed_set_comp (set_in_monotone_function Y Y x) D). Proof. use make_lub. - exact (x ,, ⨆ D). - split. + abstract (intro i ; refine (idpath _ ,, _) ; cbn in * ; apply (less_than_dcpo_lub _ _ i (refl_dcpo _))). + abstract (intros y Hy ; cbn in y, Hy ; induction y as [ x' y' ] ; cbn in * ; assert (p : x = x') ; [ assert (w := directed_set_el D) ; revert w ; use factor_through_squash ; [ apply setproperty | ] ; intro i ; exact (pr1 (Hy i)) | ] ; induction p ; refine (idpath _ ,, _) ; cbn ; use (dcpo_lub_is_least D y') ; intro i ; specialize (Hy i) ; induction Hy as [ p q ] ; assert (idpath _ = p) as r by apply setproperty ; induction r ; cbn in * ; exact q). 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.