Proposition is_scott_continuous_set_coproduct_map {Z : dcpo} {f : ∏ (x : X), Y x → Z} (Pf : ∏ (x : X), is_scott_continuous (Y x) Z (f x)) : is_scott_continuous coproduct_set_dcpo Z (λ xy, f (pr1 xy) (pr2 xy)). Proof. use make_is_scott_continuous. - exact (λ xy₁ xy₂ p, is_monotone_set_coproduct_map Y Y (λ x, pr1 (Pf x)) xy₁ xy₂ p). - intros D. assert (D' := directed_set_coproduct_set_with_eq D). revert D'. use factor_through_squash. { apply (pr1 Z). } intros D'. induction D' as [ x [ D' [ HD' H ]]]. pose (DX := make_directed_set _ _ D' HD'). assert (⨆ D = x ,, ⨆ DX) as q. { use (eq_lub coproduct_set_dcpo D _ (pr1 H)). apply is_least_upperbound_dcpo_lub. } rewrite q. cbn. refine (scott_continuous_map_on_lub (f x ,, Pf x) DX @ _). use antisymm_dcpo. + use dcpo_lub_is_least. intro i ; cbn. use less_than_dcpo_lub. * exact i. * cbn. rewrite (pr2 H i) ; cbn. apply refl_dcpo. + use dcpo_lub_is_least. intro i ; cbn. use less_than_dcpo_lub. * exact i. * cbn. rewrite (pr2 H i) ; cbn. apply refl_dcpo. 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.