proposition: Proposition is_lub_all_inl_directed_set_to_left : is_least_upperbound (coproduct_PartialOrder X Y) D (inl (⨆ all_inl_directed_set_to_left)).
proof: Proof. split. - intros i. assert (p := H i). revert p. use factor_through_squash. { apply propproperty. } intro p. induction p as [ x p ]. rewrite p. use (less_than_dcpo_lub all_inl_directed_set_to_left _ i). cbn. rewrite (all_inl_directed_set_map_eq i x p). apply refl_dcpo. - intros y Hy. induction y as [ x | y ]. + use dcpo_lub_is_least ; cbn. intro i. pose (Hy i) as p. cbn in p. assert (H' := H i). revert H'. use factor_through_squash. { apply propproperty. } intros H'. induction H' as [ x' H' ]. rewrite H' in p. cbn in p. rewrite (all_inl_directed_set_map_eq i x' H'). exact p. + cbn. assert (el := directed_set_el D). revert el. use factor_through_squash. { apply isapropempty. } intro i. assert (H' := H i). revert H'. use factor_through_squash. { apply isapropempty. } intros H'. induction H' as [ x H' ]. pose (Hy i) as p. cbn in p. rewrite H' in p. exact p. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous