Definition directed_set_coproduct_with_eq : ((∑ (D' : D → X) (HD : is_directed X D'), let DX := make_directed_set _ D D' HD in (is_least_upperbound (coproduct_PartialOrder X Y) D (inl (⨆ DX))) × (∏ (i : D), D i = inl (D' i))) ∨ (∑ (D' : D → Y) (HD : is_directed Y D'), let DY := make_directed_set _ D D' HD in is_least_upperbound (coproduct_PartialOrder X Y) D (inr (⨆ DY)) × (∏ (i : D), D i = inr (D' i))))%type. 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 ]. - use hinhpr. use inl. refine (all_inl_directed_set_map H ,, _). refine (is_directed_all_inl_directed_set_to_left H ,, _). split. + apply is_lub_all_inl_directed_set_to_left. + intro i. assert (p := H i). revert p. use factor_through_squash. { apply setproperty. } intros xH. induction xH as [ x p ]. rewrite (all_inl_directed_set_map_eq H i x p). exact p. - use hinhpr. use inr. refine (all_inr_directed_set_map H ,, _). refine (is_directed_all_inr_directed_set_to_right H ,, _). split. + apply is_lub_all_inr_directed_set_to_right. + intro i. assert (p := H i). revert p. use factor_through_squash. { apply setproperty. } intros xH. induction xH as [ x p ]. rewrite (all_inr_directed_set_map_eq H i x 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.