Proposition isaset_scott_open_set (D : dcpo) : isaset (scott_open_set D). Proof. use isaset_total2. - use funspace_isaset. exact isasethProp. - intro P. use isasetaprop. apply propproperty. Qed.
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.