Proposition is_scott_continuous_to_unit {X : hSet} (DX : dcpo_struct X) : is_scott_continuous DX unit_dcpo_struct (λ _, tt). Proof. split. - intros x y p. exact tt. - intros I D HD x Hx. split. + intro ; cbn. exact tt. + intros ? ? ; cbn. exact tt. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.