Definition directed_set_coproduct_set_with_eq : ∃ (x : X), ∑ (D' : D → Y x) (HD : is_directed (Y x) D'), let DX := make_directed_set _ D D' HD in is_least_upperbound (coproduct_set_PartialOrder _ (λ x, Y x)) D (x ,, ⨆ DX) × (∏ (i : D), D i = (x ,, D' i)). Proof. assert (h := directed_set_all_incl). revert h. use factor_through_squash. { apply propproperty. } intros xH. induction xH as [ x H ]. refine (hinhpr (x ,, _)). refine (directed_set_point_map x H ,, _). refine (is_directed_directed_set_point x H ,, _). split. - apply is_lub_directed_set_point. - intro i. assert (p := H i). revert p. use factor_through_squash. { apply setproperty. } intros yH. induction yH as [ y p ]. rewrite (directed_set_point_map_eq x H i y p). exact p. 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.