proposition: Proposition is_scott_continuous_map_from_discrete_dcpo {A : hSet} {X : dcpo} (f : A → X) : is_scott_continuous (pr2 (discrete_dcpo A)) (pr2 X) f.
proof: Proof. use make_is_scott_continuous. - apply (pr2 (monotone_function_discrete_dcpo X f)). - intros D. assert (H := directed_set_el D). revert H. use factor_through_squash. { apply setproperty. } cbn ; intros i. rewrite (discrete_dcpo_lub D i). use antisymm_dcpo. + use less_than_dcpo_lub. * exact i. * cbn. apply refl_dcpo. + use dcpo_lub_is_least. intro j ; cbn. cbn in *. assert (H := directed_set_top D i j). revert H. use factor_through_squash. { apply propproperty. } cbn ; intros H. induction H as [ k [ p q ]]. rewrite p, q. apply refl_dcpo. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous