Definition scott_continuous_map_PartialOrder (X Y : dcpo) : PartialOrder (scott_continuous_map_hSet X Y). Proof. use make_PartialOrder. - exact (λ f g, ∀ (x : X), pr1 f x ⊑ pr1 g x). - refine ((_ ,, _) ,, _). + abstract (intros f g h p q x ; exact (trans_dcpo (p x) (q x))). + abstract (intros f x ; exact (refl_dcpo (pr1 f x))). + abstract (intros f g p q ; use subtypePath ; [ intro ; apply isaprop_is_scott_continuous | ] ; use funextsec ; intro x ; exact (antisymm_dcpo (p x) (q x))). Defined.
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.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.FubiniTheorem. Require Import UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity. Require Import UniMath.OrderTheory.DCPOs.Examples.BinaryProducts.