Definition directed_set_coproduct : (∑ (D' : directed_set X), is_least_upperbound (coproduct_PartialOrder X Y) D (inl (⨆ D'))) ∨ (∑ (D' : directed_set Y), is_least_upperbound (coproduct_PartialOrder X Y) D (inr (⨆ D'))). Proof. assert (h := directed_set_all_inl_or_all_inr). revert h. use factor_through_squash. { apply propproperty. } intros H. destruct H as [ H | H ]. - refine (hinhpr (inl (all_inl_directed_set_to_left H ,, _))). apply is_lub_all_inl_directed_set_to_left. - refine (hinhpr (inr (all_inr_directed_set_to_right H ,, _))). apply is_lub_all_inr_directed_set_to_right. 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.