Proposition is_scott_continuous_sumofmaps {Z : dcpo} {f : X → Z} (Pf : is_scott_continuous X Z f) {g : Y → Z} (Pg : is_scott_continuous Y Z g) : is_scott_continuous coproduct_dcpo Z (sumofmaps f g). Proof. use make_is_scott_continuous. - exact (is_monotone_sumofmaps _ _ (pr1 Pf) (pr1 Pg)). - intros D. assert (D' := directed_set_coproduct_with_eq D). revert D'. use factor_through_squash. { apply (pr1 Z). } intros D'. induction D' as [ D' | D' ]. + induction D' as [ D' [ HD' [ H p ]]]. pose (DX := make_directed_set _ _ D' HD'). assert (⨆ D = inl (⨆ DX)) as q. { use (eq_lub coproduct_dcpo D _ H). apply is_least_upperbound_dcpo_lub. } rewrite q. cbn. refine (scott_continuous_map_on_lub (f ,, Pf) DX @ _). use antisymm_dcpo. * use dcpo_lub_is_least. intro i ; cbn. use less_than_dcpo_lub. ** exact i. ** cbn. rewrite p ; cbn. apply refl_dcpo. * use dcpo_lub_is_least. intro i ; cbn. use less_than_dcpo_lub. ** exact i. ** cbn. rewrite p ; cbn. apply refl_dcpo. + induction D' as [ D' [ HD' [ H p ]]]. pose (DY := make_directed_set _ _ D' HD'). assert (⨆ D = inr (⨆ DY)) as q. { use (eq_lub coproduct_dcpo D _ H). apply is_least_upperbound_dcpo_lub. } rewrite q. cbn. refine (scott_continuous_map_on_lub (g ,, Pg) DY @ _). use antisymm_dcpo. * use dcpo_lub_is_least. intro i ; cbn. use less_than_dcpo_lub. ** exact i. ** cbn. rewrite p ; cbn. apply refl_dcpo. * use dcpo_lub_is_least. intro i ; cbn. use less_than_dcpo_lub. ** exact i. ** cbn. rewrite p ; 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.