Proposition map_from_basis_lub (D : directed_set X) : map_from_basis (⨆ D) = ⨆_{ D} (map_from_basis ,, map_from_basis_monotone). Proof. unfold map_from_basis. use antisymm_dcpo. - unfold map_from_basis. use dcpo_lub_is_least ; cbn. intro i. induction i as [ i p ] ; cbn. assert (H := unary_interpolation CX p). revert H. use factor_through_squash. { apply propproperty. } intro H. induction H as [ j [ q₁ q₂ ]]. assert (H := q₂ D (refl_dcpo _)). revert H. use factor_through_squash. { apply propproperty. } intro k. induction k as [ k r ]. use less_than_dcpo_lub. + exact k. + cbn. use less_than_dcpo_lub. * refine (i ,, _). exact (trans_way_below_le q₁ r). * cbn. apply refl_dcpo. - unfold map_from_basis. use dcpo_lub_is_least ; cbn. intro i. use dcpo_lub_is_least ; cbn. intro j. induction j as [ j p ] ; cbn. use less_than_dcpo_lub. + refine (j ,, _). refine (trans_way_below_le p _). use less_than_dcpo_lub. * exact i. * apply refl_dcpo. + cbn. apply refl_dcpo. Qed.
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. Section ScottContinuousFromBasis. End ScottContinuousFromBasis.