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. 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.
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.