Proposition eq_strict_scott_continuous_map {X Y : dcppo} {f g : strict_scott_continuous_map X Y} (p : ∏ (x : X), f x = g x) : f = g. Proof. use subtypePath. { intro. apply isaprop_is_strict_scott_continuous. } use funextsec. exact p. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness.