Definition true_scott_open_set (A : dcpo) : scott_open_set A. Proof. simple refine (_ ,, _). - exact (λ _, htrue). - split. + abstract (intros x y p q ; exact tt). + abstract (intros D x ; assert (H := directed_set_el D) ; revert H ; use factor_through_squash_hProp ; intro d ; exact (hinhpr (d ,, tt))). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.