Proposition is_lub_all_inr_directed_set_to_right : is_least_upperbound (coproduct_PartialOrder X Y) D (inr (⨆ all_inr_directed_set_to_right)). Proof. split. - intros i. assert (p := H i). revert p. use factor_through_squash. { apply propproperty. } intro p. induction p as [ y p ]. rewrite p. use (less_than_dcpo_lub all_inr_directed_set_to_right _ i). cbn. rewrite (all_inr_directed_set_map_eq i y p). apply refl_dcpo. - intros y Hy. induction y as [ x | y ]. + 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 [ y' H' ]. pose (Hy i) as p. cbn in p. rewrite H' in p. exact p. + 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 [ y' H' ]. rewrite H' in p. cbn in p. rewrite (all_inr_directed_set_map_eq i y' H'). 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.