proposition: Proposition is_scott_continuous_to_unit {X : hSet} (DX : dcpo_struct X) : is_scott_continuous DX unit_dcpo_struct (λ _, tt).
proof: Proof. split. - intros x y p. exact tt. - intros I D HD x Hx. split. + intro ; cbn. exact tt. + intros ? ? ; cbn. exact tt. 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