Definition scott_continuous_map_from_compact_basis_ump {X : dcpo} (B : compact_basis X) {Y : dcpo} (f : B → Y) (Hf : ∏ (i₁ i₂ : B), B i₁ ≪ B i₂ → f i₁ ⊑ f i₂) : ∃! (g : scott_continuous_map X Y), ∏ (i : B), g (B i) = f i. Proof. pose (CB := compact_basis_to_dcpo_basis B). use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; use impred ; intro ; apply setproperty | ] ; use (scott_continuous_map_eq_on_basis CB) ; intro i ; exact (pr2 φ₁ i @ !(pr2 φ₂ i))). - refine (scott_continuous_map_from_basis CB f Hf ,, _). apply scott_continuous_map_from_compact_basis_eq. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. 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.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis.