Proposition is_lub_directed_set_point : is_least_upperbound (coproduct_set_PartialOrder _ (λ x, Y x)) D (x ,, ⨆ directed_set_point). 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. refine (idpath _ ,, _) ; cbn. use (less_than_dcpo_lub directed_set_point _ i) ; cbn. rewrite (directed_set_point_map_eq _ _ p). apply refl_dcpo. - intros y Hy ; cbn. induction y as [ x' y' ]. cbn in *. assert (p : x = x'). { assert (el := directed_set_el D). revert el. use factor_through_squash. { apply setproperty. } intro i. assert (H' := H i). revert H'. use factor_through_squash. { apply setproperty. } intros H'. induction H' as [ z H' ]. pose (Hy i) as p. cbn in p. rewrite H' in p. exact (pr1 p). } induction p. refine (idpath _ ,, _) ; cbn. use dcpo_lub_is_least. 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 ; cbn. rewrite (directed_set_point_map_eq i _ H'). induction p as [ p q ]. assert (r : idpath _ = p) by apply setproperty. induction r. exact q. 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.